Next Prev Up
BfEqvBfRule

⊢ f ≡ g ⇒ ⊢ f ≡ g BfEqvBfRule

Proof:

1
f ≡ g
Assump
2
f ⊃ g
1,Prop
3
f ⊃ g
2,BfImpBfRule
4
g ⊃ f
1,Prop
5
g ⊃ f
4,BfImpBfRule
6
f ≡ g
3, 5,Prop

qed

Next Prev Up

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