| ⊢ (f ≡ g) ≡ (f ⊃ g) ∧ (g ⊃ f) | BfEqvSplit |
Proof:
1 | (f ≡ g) ≡ (f ⊃ g) ∧ (g ⊃ f) | |
2 | (f ≡ g) ≡ ((f ⊃ g) ∧ (g ⊃ f)) | |
3 | ((f ⊃ g) ∧ (g ⊃ f)) ≡ (f ⊃ g) ∧ (g ⊃ f) | |
4 | (f ≡ g) ≡ (f ⊃ g) ∧ (g ⊃ f) |
qed