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  4357  fimacnvdisj  5366  fvimacnv  5594  ssct  6775  f1vrnfibi  6901  inl11  7021  ctssdc  7069  enomnilem  7093  enmkvlem  7116  djuen  7158  cauappcvgprlemlol  7579  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  caucvgprlemlol  7602  caucvgprlemladdrl  7610  caucvgprprlemlol  7630  suplocsrlem  7740  recgt1i  8784  avgle2  9089  xnn0le2is012  9793  ioodisj  9920  fzneuz  10026  fihashfn  10702  shftfvalg  10746  shftfval  10749  cvg1nlemres  10913  resqrexlem1arp  10933  maxabslemval  11136  xrmaxiflemval  11177  xrmaxadd  11188  xrminmax  11192  summodclem3  11307  fsumsplit  11334  mertenslemub  11461  fprodsplit  11524  demoivreALT  11700  zsupcllemstep  11863  gcdsupex  11875  gcdsupcl  11876  gcdneg  11900  bezoutlemsup  11927  eucalginv  11967  eucalg  11970  odzdvds  12154  fldivp1  12255  enctlem  12302  ctiunctlemfo  12309  iscnp4  12759  cnntr  12766  tx2cn  12811  hmeontr  12854  hmeores  12856  xmetres2  12920  metres2  12922  limccnp2cntop  13187  limccoap  13188  isomninnlem  13743  iswomninnlem  13762  ismkvnnlem  13765