This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem biancomi

Description: Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018)

Ref Expression
Hypothesis biancomi.1 ⊢ ( 𝜑 ↔ ( 𝜒 ∧ 𝜓 ) )
Assertion biancomi ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 biancomi.1 ⊢ ( 𝜑 ↔ ( 𝜒 ∧ 𝜓 ) )
2 ancom ⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜒 ∧ 𝜓 ) )
3 1 2 bitr4i ⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )