BiImpDiImpDi

⊢ (f ⊃ g) ⊃ f ⊃ g BiImpDiImpDi

Proof:

1
⊢ (f ⊃ g) ⊃ (f ; true) ⊃ (g ; true)
2
⊢ (f ⊃ g) ⊃ f ⊃ g
1, def. of 

qed

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