Metamath Proof Explorer


Theorem aibandbiaiaiffb

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

Ref Expression
Assertion aibandbiaiaiffb φ ψ ψ φ φ ψ

Proof

Step Hyp Ref Expression
1 dfbi2 φ ψ φ ψ ψ φ
2 1 biimpri φ ψ ψ φ φ ψ