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

Metamath Proof Explorer

Theorem bitr3id

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

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

Proof

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