Metamath Proof Explorer

Theorem biantr

Description: A transitive law of equivalence. Compare Theorem *4.22 of WhiteheadRussell p. 117. (Contributed by NM, 18-Aug-1993)

Ref Expression
Assertion biantr ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜓 ) ) → ( 𝜑 ↔ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( ( 𝜒 ↔ 𝜓 ) → ( 𝜒 ↔ 𝜓 ) )
2 1 bibi2d ⊢ ( ( 𝜒 ↔ 𝜓 ) → ( ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
3 2 biimparc ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜓 ) ) → ( 𝜑 ↔ 𝜒 ) )