Theorem sylancom 418

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ordin  4368  fimacnvdisj  5380  fvimacnv  5608  ssct  6792  f1vrnfibi  6918  inl11  7038  ctssdc  7086  enomnilem  7110  enmkvlem  7133  djuen  7175  cauappcvgprlemlol  7596  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  caucvgprlemlol  7619  caucvgprlemladdrl  7627  caucvgprprlemlol  7647  suplocsrlem  7757  recgt1i  8801  avgle2  9106  xnn0le2is012  9810  ioodisj  9937  fzneuz  10044  fihashfn  10722  shftfvalg  10769  shftfval  10772  cvg1nlemres  10936  resqrexlem1arp  10956  maxabslemval  11159  xrmaxiflemval  11200  xrmaxadd  11211  xrminmax  11215  summodclem3  11330  fsumsplit  11357  mertenslemub  11484  fprodsplit  11547  demoivreALT  11723  zsupcllemstep  11887  gcdsupex  11899  gcdsupcl  11900  gcdneg  11924  bezoutlemsup  11951  eucalginv  11997  eucalg  12000  odzdvds  12186  fldivp1  12287  prmunb  12301  enctlem  12374  ctiunctlemfo  12381  intopsn  12608  iscnp4  12971  cnntr  12978  tx2cn  13023  hmeontr  13066  hmeores  13068  xmetres2  13132  metres2  13134  limccnp2cntop  13399  limccoap  13400  isomninnlem  14022  iswomninnlem  14041  ismkvnnlem  14044