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  4175  fimacnvdisj  5142  fvimacnv  5358  ssct  6463  f1vrnfibi  6578  enomnilem  6698  cauappcvgprlemlol  7108  cauappcvgprlemladdru  7117  cauappcvgprlemladdrl  7118  caucvgprlemlol  7131  caucvgprlemladdrl  7139  caucvgprprlemlol  7159  recgt1i  8252  avgle2  8548  ioodisj  9304  fzneuz  9407  fihashfn  10042  shftfvalg  10079  shftfval  10082  cvg1nlemres  10244  resqrexlem1arp  10264  maxabslemval  10467  zsupcllemstep  10720  gcdsupex  10728  gcdsupcl  10729  gcdneg  10752  bezoutlemsup  10777  eucalginv  10817  eucialg  10820