Next Prev Up
DiImpDi

⊢ f ⊃ g ⇒ ⊢ f ⊃ g DiImpDi

Proof:

1
⊢ f ⊃ g
given
2
⊢ f ; true ⊃ g ; true
1,LeftChopImpChop
3
⊢ f ⊃ g
2, def. of 

qed

Another corollary is the following:

Next Prev Up

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023