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  4440  fimacnvdisj  5472  fvimacnv  5708  ssct  6928  f1vrnfibi  7062  inl11  7182  ctssdc  7230  enomnilem  7255  enmkvlem  7278  djuen  7339  cauappcvgprlemlol  7780  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgprlemlol  7803  caucvgprlemladdrl  7811  caucvgprprlemlol  7831  suplocsrlem  7941  recgt1i  8991  avgle2  9299  xnn0le2is012  10008  ioodisj  10135  fzneuz  10243  zsupcllemstep  10394  fihashfn  10967  shftfvalg  11204  shftfval  11207  cvg1nlemres  11371  resqrexlem1arp  11391  maxabslemval  11594  xrmaxiflemval  11636  xrmaxadd  11647  xrminmax  11651  summodclem3  11766  fsumsplit  11793  mertenslemub  11920  fprodsplit  11983  demoivreALT  12160  bitsp1  12337  gcdneg  12378  bezoutlemsup  12405  eucalginv  12453  eucalg  12456  odzdvds  12643  pclemdc  12686  fldivp1  12746  prmunb  12760  enctlem  12878  ctiunctlemfo  12885  pwssnf1o  13205  intopsn  13274  grpsubval  13453  mulgnndir  13562  gsumfzreidx  13748  gsumfzmptfidmadd  13750  znunit  14496  iscnp4  14765  cnntr  14772  tx2cn  14817  hmeontr  14860  hmeores  14862  xmetres2  14926  metres2  14928  limccnp2cntop  15224  limccoap  15225  isomninnlem  16110  iswomninnlem  16129  ismkvnnlem  16132