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  4476  fimacnvdisj  5512  fvimacnv  5752  ssct  6983  f1vrnfibi  7123  inl11  7243  ctssdc  7291  enomnilem  7316  enmkvlem  7339  djuen  7404  cauappcvgprlemlol  7845  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemlol  7868  caucvgprlemladdrl  7876  caucvgprprlemlol  7896  suplocsrlem  8006  recgt1i  9056  avgle2  9364  eluzmn  9740  xnn0le2is012  10074  ioodisj  10201  fzneuz  10309  zsupcllemstep  10461  fihashfn  11034  shftfvalg  11345  shftfval  11348  cvg1nlemres  11512  resqrexlem1arp  11532  maxabslemval  11735  xrmaxiflemval  11777  xrmaxadd  11788  xrminmax  11792  summodclem3  11907  fsumsplit  11934  mertenslemub  12061  fprodsplit  12124  demoivreALT  12301  bitsp1  12478  gcdneg  12519  bezoutlemsup  12546  eucalginv  12594  eucalg  12597  odzdvds  12784  pclemdc  12827  fldivp1  12887  prmunb  12901  enctlem  13019  ctiunctlemfo  13026  pwssnf1o  13347  intopsn  13416  grpsubval  13595  mulgnndir  13704  gsumfzreidx  13890  gsumfzmptfidmadd  13892  znunit  14639  iscnp4  14908  cnntr  14915  tx2cn  14960  hmeontr  15003  hmeores  15005  xmetres2  15069  metres2  15071  limccnp2cntop  15367  limccoap  15368  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508