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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem is used by:  ordin  4530  fimacnvdisj  5576  fvimacnv  5824  ssct  7114  f1vrnfibi  7259  inl11  7405  ctssdc  7453  enomnilem  7478  enmkvlem  7501  djuen  7567  cauappcvgprlemlol  8014  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemlol  8037  caucvgprlemladdrl  8045  caucvgprprlemlol  8065  suplocsrlem  8175  recgt1i  9230  avgle2  9551  eluzmn  9937  xnn0le2is012  10278  ioodisj  10405  fzneuz  10518  zsupcllemstep  10672  fihashfn  11254  sseqn  11293  shftfvalg  11597  shftfval  11600  cvg1nlemres  11765  resqrexlem1arp  11785  maxabslemval  11989  xrmaxiflemval  12032  xrmaxadd  12043  xrminmax  12047  summodclem3  12163  fsumsplit  12190  mertenslemub  12317  fprodsplit  12380  demoivreALT  12557  bitsp1  12734  gcdneg  12775  bezoutlemsup  12802  eucalginv  12850  eucalg  12853  odzdvds  13044  pclemdc  13087  fldivp1  13147  prmunb  13161  ballotfilemirc  13324  enctlem  13372  ctiunctlemfo  13379  intopsn  13736  grpsubval  13900  mulgnndir  14003  gzsumreidx  14190  gsumvalfi  14201  gsumf1ofi  14209  pwssnf1o  14260  znunit  15043  iscnp4  15368  cnntr  15375  tx2cn  15420  hmeontr  15463  hmeores  15465  xmetres2  15529  metres2  15531  limccnp2cntop  15827  limccoap  15828  birthdaylem3  16146  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200