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  4450  fimacnvdisj  5482  fvimacnv  5718  ssct  6938  f1vrnfibi  7073  inl11  7193  ctssdc  7241  enomnilem  7266  enmkvlem  7289  djuen  7354  cauappcvgprlemlol  7795  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemlol  7818  caucvgprlemladdrl  7826  caucvgprprlemlol  7846  suplocsrlem  7956  recgt1i  9006  avgle2  9314  xnn0le2is012  10023  ioodisj  10150  fzneuz  10258  zsupcllemstep  10409  fihashfn  10982  shftfvalg  11244  shftfval  11247  cvg1nlemres  11411  resqrexlem1arp  11431  maxabslemval  11634  xrmaxiflemval  11676  xrmaxadd  11687  xrminmax  11691  summodclem3  11806  fsumsplit  11833  mertenslemub  11960  fprodsplit  12023  demoivreALT  12200  bitsp1  12377  gcdneg  12418  bezoutlemsup  12445  eucalginv  12493  eucalg  12496  odzdvds  12683  pclemdc  12726  fldivp1  12786  prmunb  12800  enctlem  12918  ctiunctlemfo  12925  pwssnf1o  13245  intopsn  13314  grpsubval  13493  mulgnndir  13602  gsumfzreidx  13788  gsumfzmptfidmadd  13790  znunit  14536  iscnp4  14805  cnntr  14812  tx2cn  14857  hmeontr  14900  hmeores  14902  xmetres2  14966  metres2  14968  limccnp2cntop  15264  limccoap  15265  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193