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

Metamath Proof Explorer

Theorem sylan9bbr

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

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

Proof

Step Hyp Ref Expression
1 sylan9bbr.1 ⊢ φ → ψ ↔ χ
2 sylan9bbr.2 ⊢ θ → χ ↔ τ
3 1 2 sylan9bb ⊢ φ ∧ θ → ψ ↔ τ
4 3 ancoms ⊢ θ ∧ φ → ψ ↔ τ