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  4482  fimacnvdisj  5521  fvimacnv  5762  ssct  7000  f1vrnfibi  7144  inl11  7264  ctssdc  7312  enomnilem  7337  enmkvlem  7360  djuen  7426  cauappcvgprlemlol  7867  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemlol  7890  caucvgprlemladdrl  7898  caucvgprprlemlol  7918  suplocsrlem  8028  recgt1i  9078  avgle2  9386  eluzmn  9762  xnn0le2is012  10101  ioodisj  10228  fzneuz  10336  zsupcllemstep  10490  fihashfn  11064  shftfvalg  11396  shftfval  11399  cvg1nlemres  11563  resqrexlem1arp  11583  maxabslemval  11786  xrmaxiflemval  11828  xrmaxadd  11839  xrminmax  11843  summodclem3  11959  fsumsplit  11986  mertenslemub  12113  fprodsplit  12176  demoivreALT  12353  bitsp1  12530  gcdneg  12571  bezoutlemsup  12598  eucalginv  12646  eucalg  12649  odzdvds  12836  pclemdc  12879  fldivp1  12939  prmunb  12953  enctlem  13071  ctiunctlemfo  13078  pwssnf1o  13399  intopsn  13468  grpsubval  13647  mulgnndir  13756  gsumfzreidx  13942  gsumfzmptfidmadd  13944  znunit  14692  iscnp4  14961  cnntr  14968  tx2cn  15013  hmeontr  15056  hmeores  15058  xmetres2  15122  metres2  15124  limccnp2cntop  15420  limccoap  15421  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708  gfsumval  16732