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 ( ( ( 𝜑𝜓 ) ∧ ( 𝜓𝜑 ) ) ↔ ( 𝜑𝜓 ) )