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  4433  fimacnvdisj  5462  fvimacnv  5697  ssct  6915  f1vrnfibi  7049  inl11  7169  ctssdc  7217  enomnilem  7242  enmkvlem  7265  djuen  7325  cauappcvgprlemlol  7762  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgprlemlol  7785  caucvgprlemladdrl  7793  caucvgprprlemlol  7813  suplocsrlem  7923  recgt1i  8973  avgle2  9281  xnn0le2is012  9990  ioodisj  10117  fzneuz  10225  zsupcllemstep  10374  fihashfn  10947  shftfvalg  11162  shftfval  11165  cvg1nlemres  11329  resqrexlem1arp  11349  maxabslemval  11552  xrmaxiflemval  11594  xrmaxadd  11605  xrminmax  11609  summodclem3  11724  fsumsplit  11751  mertenslemub  11878  fprodsplit  11941  demoivreALT  12118  bitsp1  12295  gcdneg  12336  bezoutlemsup  12363  eucalginv  12411  eucalg  12414  odzdvds  12601  pclemdc  12644  fldivp1  12704  prmunb  12718  enctlem  12836  ctiunctlemfo  12843  pwssnf1o  13163  intopsn  13232  grpsubval  13411  mulgnndir  13520  gsumfzreidx  13706  gsumfzmptfidmadd  13708  znunit  14454  iscnp4  14723  cnntr  14730  tx2cn  14775  hmeontr  14818  hmeores  14820  xmetres2  14884  metres2  14886  limccnp2cntop  15182  limccoap  15183  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028