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

Metamath Proof Explorer

Theorem syl3an132

Description: syl2an with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016)

Ref Expression
Hypotheses syl3an132.1 ⊢ φ → ψ
syl3an132.2 ⊢ χ ∧ θ → τ
syl3an132.3 ⊢ ψ ∧ τ → η
Assertion syl3an132 ⊢ φ ∧ χ ∧ θ → η

Proof

Step Hyp Ref Expression
1 syl3an132.1 ⊢ φ → ψ
2 syl3an132.2 ⊢ χ ∧ θ → τ
3 syl3an132.3 ⊢ ψ ∧ τ → η
4 1 2 3 syl2an ⊢ φ ∧ χ ∧ θ → η
5 4 3impb ⊢ φ ∧ χ ∧ θ → η