Metamath Proof Explorer

Theorem aibandbiaiffaiffb

Description: A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016)

Ref Expression
Assertion aibandbiaiffaiffb ⊢ φ → ψ ∧ ψ → φ ↔ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 dfbi2 ⊢ φ ↔ ψ ↔ φ → ψ ∧ ψ → φ
2 1 bicomi ⊢ φ → ψ ∧ ψ → φ ↔ φ ↔ ψ