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

Metamath Proof Explorer

Theorem bitr2di

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

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

Proof

Step Hyp Ref Expression
1 bitr2di.1 ⊢ φ → ψ ↔ χ
2 bitr2di.2 ⊢ χ ↔ θ
3 1 2 bitrdi ⊢ φ → ψ ↔ θ
4 3 bicomd ⊢ φ → θ ↔ ψ