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

Metamath Proof Explorer

Theorem sylancom

Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008)

Ref Expression
Hypotheses sylancom.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
sylancom.2 ⊢ ( ( 𝜒 ∧ 𝜓 ) → 𝜃 )
Assertion sylancom ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 sylancom.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2 sylancom.2 ⊢ ( ( 𝜒 ∧ 𝜓 ) → 𝜃 )
3 simpr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 )
4 1 3 2 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )