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  4508  fimacnvdisj  5553  fvimacnv  5795  ssct  7069  f1vrnfibi  7214  inl11  7358  ctssdc  7406  enomnilem  7431  enmkvlem  7454  djuen  7520  cauappcvgprlemlol  7964  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  caucvgprlemlol  7987  caucvgprlemladdrl  7995  caucvgprprlemlol  8015  suplocsrlem  8125  recgt1i  9174  avgle2  9482  eluzmn  9863  xnn0le2is012  10202  ioodisj  10329  fzneuz  10439  zsupcllemstep  10593  fihashfn  11168  sseqn  11207  shftfvalg  11507  shftfval  11510  cvg1nlemres  11674  resqrexlem1arp  11694  maxabslemval  11897  xrmaxiflemval  11939  xrmaxadd  11950  xrminmax  11954  summodclem3  12070  fsumsplit  12097  mertenslemub  12224  fprodsplit  12287  demoivreALT  12464  bitsp1  12641  gcdneg  12682  bezoutlemsup  12709  eucalginv  12757  eucalg  12760  odzdvds  12947  pclemdc  12990  fldivp1  13050  prmunb  13064  enctlem  13200  ctiunctlemfo  13207  pwssnf1o  13528  intopsn  13597  grpsubval  13776  mulgnndir  13885  gsumfzreidx  14071  gsumfzmptfidmadd  14073  znunit  14824  iscnp4  15100  cnntr  15107  tx2cn  15152  hmeontr  15195  hmeores  15197  xmetres2  15261  metres2  15263  limccnp2cntop  15559  limccoap  15560  isomninnlem  16831  iswomninnlem  16851  ismkvnnlem  16854  gfsumval  16879