Metamath Proof Explorer


Theorem biancomd

Description: Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018)

Ref Expression
Hypothesis biancomd.1 ( 𝜑 → ( 𝜓 ↔ ( 𝜃𝜒 ) ) )
Assertion biancomd ( 𝜑 → ( 𝜓 ↔ ( 𝜒𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 biancomd.1 ( 𝜑 → ( 𝜓 ↔ ( 𝜃𝜒 ) ) )
2 ancom ( ( 𝜃𝜒 ) ↔ ( 𝜒𝜃 ) )
3 1 2 bitrdi ( 𝜑 → ( 𝜓 ↔ ( 𝜒𝜃 ) ) )