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

Metamath Proof Explorer

Theorem bitrid

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypotheses bitrid.1 ⊢ φ ↔ ψ
bitrid.2 ⊢ χ → ψ ↔ θ
Assertion bitrid ⊢ χ → φ ↔ θ

Proof

Step Hyp Ref Expression
1 bitrid.1 ⊢ φ ↔ ψ
2 bitrid.2 ⊢ χ → ψ ↔ θ
3 1 a1i ⊢ χ → φ ↔ ψ
4 3 2 bitrd ⊢ χ → φ ↔ θ