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

Metamath Proof Explorer

Theorem syl3an12

Description: A double syllogism inference. (Contributed by SN, 15-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 syl3an12.1 ⊢ φ → ψ
2 syl3an12.2 ⊢ χ → θ
3 syl3an12.s ⊢ ψ ∧ θ ∧ τ → η
4 id ⊢ τ → τ
5 1 2 4 3 syl3an ⊢ φ ∧ χ ∧ τ → η