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

Metamath Proof Explorer

Theorem bitr2d

Description: Deduction form of bitr2i . (Contributed by NM, 9-Jun-2004)

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

Proof

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