Theorem sylancom 420

Description: Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)

Hypotheses

Ref	Expression
sylancom.1	|- ( ( ph /\ ps ) -> ch )
sylancom.2	|- ( ( ch /\ ps ) -> th )

Assertion

Ref	Expression
sylancom	|- ( ( ph /\ ps ) -> th )

Proof of Theorem sylancom

Step	Hyp	Ref	Expression
1		sylancom.1	. 2 |- ( ( ph /\ ps ) -> ch )
2		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
3		sylancom.2	. 2 |- ( ( ch /\ ps ) -> th )
4	1, 2, 3	syl2anc 411	1 |- ( ( ph /\ ps ) -> th )

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  4416  fimacnvdisj  5438  fvimacnv  5673  ssct  6872  f1vrnfibi  7004  inl11  7124  ctssdc  7172  enomnilem  7197  enmkvlem  7220  djuen  7271  cauappcvgprlemlol  7707  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemlol  7730  caucvgprlemladdrl  7738  caucvgprprlemlol  7758  suplocsrlem  7868  recgt1i  8917  avgle2  9224  xnn0le2is012  9932  ioodisj  10059  fzneuz  10167  fihashfn  10871  shftfvalg  10962  shftfval  10965  cvg1nlemres  11129  resqrexlem1arp  11149  maxabslemval  11352  xrmaxiflemval  11393  xrmaxadd  11404  xrminmax  11408  summodclem3  11523  fsumsplit  11550  mertenslemub  11677  fprodsplit  11740  demoivreALT  11917  zsupcllemstep  12082  gcdneg  12119  bezoutlemsup  12146  eucalginv  12194  eucalg  12197  odzdvds  12383  pclemdc  12426  fldivp1  12486  prmunb  12500  enctlem  12589  ctiunctlemfo  12596  intopsn  12950  grpsubval  13118  mulgnndir  13221  gsumfzreidx  13407  gsumfzmptfidmadd  13409  znunit  14147  iscnp4  14386  cnntr  14393  tx2cn  14438  hmeontr  14481  hmeores  14483  xmetres2  14547  metres2  14549  limccnp2cntop  14831  limccoap  14832  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542