Theorem sylancom 411

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

Hypotheses

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

Assertion

Ref	Expression
sylancom	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem sylancom

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

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  ordin  4186  fimacnvdisj  5158  fvimacnv  5377  ssct  6486  f1vrnfibi  6604  enomnilem  6738  cauappcvgprlemlol  7150  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprlemlol  7173  caucvgprlemladdrl  7181  caucvgprprlemlol  7201  recgt1i  8294  avgle2  8590  ioodisj  9342  fzneuz  9445  fihashfn  10104  shftfvalg  10148  shftfval  10151  cvg1nlemres  10313  resqrexlem1arp  10333  maxabslemval  10536  isummolem3  10659  zsupcllemstep  10816  gcdsupex  10824  gcdsupcl  10825  gcdneg  10848  bezoutlemsup  10873  eucalginv  10913  eucialg  10916