Theorem sylancom 420

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 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 411	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  ordin  4387  fimacnvdisj  5402  fvimacnv  5633  ssct  6820  f1vrnfibi  6946  inl11  7066  ctssdc  7114  enomnilem  7138  enmkvlem  7161  djuen  7212  cauappcvgprlemlol  7648  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemlol  7671  caucvgprlemladdrl  7679  caucvgprprlemlol  7699  suplocsrlem  7809  recgt1i  8857  avgle2  9162  xnn0le2is012  9868  ioodisj  9995  fzneuz  10103  fihashfn  10782  shftfvalg  10829  shftfval  10832  cvg1nlemres  10996  resqrexlem1arp  11016  maxabslemval  11219  xrmaxiflemval  11260  xrmaxadd  11271  xrminmax  11275  summodclem3  11390  fsumsplit  11417  mertenslemub  11544  fprodsplit  11607  demoivreALT  11783  zsupcllemstep  11948  gcdsupex  11960  gcdsupcl  11961  gcdneg  11985  bezoutlemsup  12012  eucalginv  12058  eucalg  12061  odzdvds  12247  fldivp1  12348  prmunb  12362  enctlem  12435  ctiunctlemfo  12442  intopsn  12791  grpsubval  12924  mulgnndir  13017  iscnp4  13757  cnntr  13764  tx2cn  13809  hmeontr  13852  hmeores  13854  xmetres2  13918  metres2  13920  limccnp2cntop  14185  limccoap  14186  isomninnlem  14817  iswomninnlem  14836  ismkvnnlem  14839