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  4386  fimacnvdisj  5401  fvimacnv  5632  ssct  6818  f1vrnfibi  6944  inl11  7064  ctssdc  7112  enomnilem  7136  enmkvlem  7159  djuen  7210  cauappcvgprlemlol  7646  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemlol  7669  caucvgprlemladdrl  7677  caucvgprprlemlol  7697  suplocsrlem  7807  recgt1i  8855  avgle2  9160  xnn0le2is012  9866  ioodisj  9993  fzneuz  10101  fihashfn  10780  shftfvalg  10827  shftfval  10830  cvg1nlemres  10994  resqrexlem1arp  11014  maxabslemval  11217  xrmaxiflemval  11258  xrmaxadd  11269  xrminmax  11273  summodclem3  11388  fsumsplit  11415  mertenslemub  11542  fprodsplit  11605  demoivreALT  11781  zsupcllemstep  11946  gcdsupex  11958  gcdsupcl  11959  gcdneg  11983  bezoutlemsup  12010  eucalginv  12056  eucalg  12059  odzdvds  12245  fldivp1  12346  prmunb  12360  enctlem  12433  ctiunctlemfo  12440  intopsn  12786  grpsubval  12919  mulgnndir  13012  iscnp4  13721  cnntr  13728  tx2cn  13773  hmeontr  13816  hmeores  13818  xmetres2  13882  metres2  13884  limccnp2cntop  14149  limccoap  14150  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803