equi_symm

Theorem equi_symm

Theorem. equi_symm
(A ↔ B) → (B ↔ A)

Proof
01. 1 ⊢ A ↔ B, hypo.
02. 1 ⊢ A → B, bij_eliml 1.
03. 1 ⊢ B → A, bij_elimr 1.
04. 1 ⊢ B ↔ A, bij_intro 3 2.
equi_symm. ⊢ (A ↔ B) → (B ↔ A), subj_intro 4.