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

Metamath Proof Explorer

Theorem sylan9bb

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995)

Ref Expression
Hypotheses sylan9bb.1 ⊢ φ → ψ ↔ χ
sylan9bb.2 ⊢ θ → χ ↔ τ
Assertion sylan9bb ⊢ φ ∧ θ → ψ ↔ τ

Proof

Step Hyp Ref Expression
1 sylan9bb.1 ⊢ φ → ψ ↔ χ
2 sylan9bb.2 ⊢ θ → χ ↔ τ
3 1 adantr ⊢ φ ∧ θ → ψ ↔ χ
4 2 adantl ⊢ φ ∧ θ → χ ↔ τ
5 3 4 bitrd ⊢ φ ∧ θ → ψ ↔ τ