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

Metamath Proof Explorer

Theorem bitr3di

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994)

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

Proof

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