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  4421  fimacnvdisj  5445  fvimacnv  5680  ssct  6886  f1vrnfibi  7020  inl11  7140  ctssdc  7188  enomnilem  7213  enmkvlem  7236  djuen  7294  cauappcvgprlemlol  7731  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemlol  7754  caucvgprlemladdrl  7762  caucvgprprlemlol  7782  suplocsrlem  7892  recgt1i  8942  avgle2  9250  xnn0le2is012  9958  ioodisj  10085  fzneuz  10193  zsupcllemstep  10336  fihashfn  10909  shftfvalg  11000  shftfval  11003  cvg1nlemres  11167  resqrexlem1arp  11187  maxabslemval  11390  xrmaxiflemval  11432  xrmaxadd  11443  xrminmax  11447  summodclem3  11562  fsumsplit  11589  mertenslemub  11716  fprodsplit  11779  demoivreALT  11956  bitsp1  12133  gcdneg  12174  bezoutlemsup  12201  eucalginv  12249  eucalg  12252  odzdvds  12439  pclemdc  12482  fldivp1  12542  prmunb  12556  enctlem  12674  ctiunctlemfo  12681  pwssnf1o  13000  intopsn  13069  grpsubval  13248  mulgnndir  13357  gsumfzreidx  13543  gsumfzmptfidmadd  13545  znunit  14291  iscnp4  14538  cnntr  14545  tx2cn  14590  hmeontr  14633  hmeores  14635  xmetres2  14699  metres2  14701  limccnp2cntop  14997  limccoap  14998  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783