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  4532  fimacnvdisj  5579  fvimacnv  5827  ssct  7120  f1vrnfibi  7265  inl11  7411  ctssdc  7459  enomnilem  7484  enmkvlem  7507  djuen  7573  cauappcvgprlemlol  8020  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemlol  8043  caucvgprlemladdrl  8051  caucvgprprlemlol  8071  suplocsrlem  8181  recgt1i  9236  avgle2  9558  eluzmn  9943  xnn0le2is012  10284  ioodisj  10411  fzneuz  10524  zsupcllemstep  10678  fihashfn  11261  sseqn  11300  shftfvalg  11604  shftfval  11607  cvg1nlemres  11772  resqrexlem1arp  11792  maxabslemval  11996  xrmaxiflemval  12040  xrmaxadd  12051  xrminmax  12055  summodclem3  12171  fsumsplit  12198  mertenslemub  12325  fprodsplit  12388  demoivreALT  12565  bitsp1  12742  gcdneg  12783  bezoutlemsup  12810  eucalginv  12858  eucalg  12861  odzdvds  13052  pclemdc  13095  fldivp1  13155  prmunb  13169  ballotfilemirc  13332  enctlem  13380  ctiunctlemfo  13387  intopsn  13745  grpsubval  13909  mulgnndir  14012  cntzidss  14171  gzsumreidx  14230  gsumvalfi  14241  gsumf1ofi  14249  pwssnf1o  14317  znunit  15102  iscnp4  15461  cnntr  15468  tx2cn  15513  hmeontr  15556  hmeores  15558  xmetres2  15622  metres2  15624  limccnp2cntop  15920  limccoap  15921  birthdaylem3  16244  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326