Theorem sylancom 424

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 415	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  4525  fimacnvdisj  5571  fvimacnv  5815  ssct  7104  f1vrnfibi  7249  inl11  7395  ctssdc  7443  enomnilem  7468  enmkvlem  7491  djuen  7557  cauappcvgprlemlol  8004  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemlol  8027  caucvgprlemladdrl  8035  caucvgprprlemlol  8055  suplocsrlem  8165  recgt1i  9218  avgle2  9526  eluzmn  9907  xnn0le2is012  10247  ioodisj  10374  fzneuz  10486  zsupcllemstep  10640  fihashfn  11218  sseqn  11257  shftfvalg  11561  shftfval  11564  cvg1nlemres  11729  resqrexlem1arp  11749  maxabslemval  11952  xrmaxiflemval  11994  xrmaxadd  12005  xrminmax  12009  summodclem3  12125  fsumsplit  12152  mertenslemub  12279  fprodsplit  12342  demoivreALT  12519  bitsp1  12696  gcdneg  12737  bezoutlemsup  12764  eucalginv  12812  eucalg  12815  odzdvds  13002  pclemdc  13045  fldivp1  13105  prmunb  13119  ballotfilemirc  13253  enctlem  13301  ctiunctlemfo  13308  intopsn  13664  grpsubval  13828  mulgnndir  13931  gzsumreidx  14118  gsumvalfi  14129  gsumf1ofi  14137  pwssnf1o  14188  znunit  14966  iscnp4  15242  cnntr  15249  tx2cn  15294  hmeontr  15337  hmeores  15339  xmetres2  15403  metres2  15405  limccnp2cntop  15701  limccoap  15702  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007