Theorem sylancom 417

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 109	. 2 |- ( ( ph /\ ps ) -> ps )
3		sylancom.2	. 2 |- ( ( ch /\ ps ) -> th )
4	1, 2, 3	syl2anc 409	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ordin  4363  fimacnvdisj  5372  fvimacnv  5600  ssct  6784  f1vrnfibi  6910  inl11  7030  ctssdc  7078  enomnilem  7102  enmkvlem  7125  djuen  7167  cauappcvgprlemlol  7588  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgprlemlol  7611  caucvgprlemladdrl  7619  caucvgprprlemlol  7639  suplocsrlem  7749  recgt1i  8793  avgle2  9098  xnn0le2is012  9802  ioodisj  9929  fzneuz  10036  fihashfn  10713  shftfvalg  10760  shftfval  10763  cvg1nlemres  10927  resqrexlem1arp  10947  maxabslemval  11150  xrmaxiflemval  11191  xrmaxadd  11202  xrminmax  11206  summodclem3  11321  fsumsplit  11348  mertenslemub  11475  fprodsplit  11538  demoivreALT  11714  zsupcllemstep  11878  gcdsupex  11890  gcdsupcl  11891  gcdneg  11915  bezoutlemsup  11942  eucalginv  11988  eucalg  11991  odzdvds  12177  fldivp1  12278  prmunb  12292  enctlem  12365  ctiunctlemfo  12372  intopsn  12598  iscnp4  12858  cnntr  12865  tx2cn  12910  hmeontr  12953  hmeores  12955  xmetres2  13019  metres2  13021  limccnp2cntop  13286  limccoap  13287  isomninnlem  13909  iswomninnlem  13928  ismkvnnlem  13931