Next Prev Up
BiImpBiRule

⊢ f ⊃ g ⇒ ⊢ f ⊃ g BiImpBiRule

Proof:

1
⊢ f ⊃ g
given
2
⊢ ¬g ⊃¬f
1,Prop
3
⊢ ¬g ⊃¬f
2,DiImpDi
4
⊢ ¬¬f ⊃¬¬g
3,Prop
5
⊢ f ⊃ g
4, def. of 

qed

Next Prev Up

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