Next Prev Up
TrueEqvTrueChopTrue

⊢ true ≡true ; true TrueEqvTrueChopTrue

Proof:

1
⊢ true ; true ⊃true
Prop
2
⊢ true ⊃true
DiIntro
3
⊢ true ⊃true ; true
2, def. of 
4
⊢ true ≡true ; true
1, 3,Prop

qed

Next Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024