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

Metamath Proof Explorer

Theorem bianim

Description: Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023)

Ref Expression
Hypotheses bianim.1 ⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )
bianim.2 ⊢ ( 𝜒 → ( 𝜓 ↔ 𝜃 ) )
Assertion bianim ( 𝜑 ↔ ( 𝜃 ∧ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 bianim.1 ⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )
2 bianim.2 ⊢ ( 𝜒 → ( 𝜓 ↔ 𝜃 ) )
3 2 pm5.32ri ⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜃 ∧ 𝜒 ) )
4 1 3 bitri ⊢ ( 𝜑 ↔ ( 𝜃 ∧ 𝜒 ) )