Next Prev Up
DfImpDf

⊢ f ⊃ g ⇒ ⊢ f ⊃ g DfImpDf

Proof:

1
f ⊃ g
Assump
2
f ⌢ true ⊃ g ⌢ true
1,LeftChopImpChop
3
f ⊃ g
2, def. of 

qed

Next Prev Up

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