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  4384  fimacnvdisj  5399  fvimacnv  5630  ssct  6815  f1vrnfibi  6941  inl11  7061  ctssdc  7109  enomnilem  7133  enmkvlem  7156  djuen  7207  cauappcvgprlemlol  7643  cauappcvgprlemladdru  7652  cauappcvgprlemladdrl  7653  caucvgprlemlol  7666  caucvgprlemladdrl  7674  caucvgprprlemlol  7694  suplocsrlem  7804  recgt1i  8851  avgle2  9156  xnn0le2is012  9862  ioodisj  9989  fzneuz  10096  fihashfn  10773  shftfvalg  10820  shftfval  10823  cvg1nlemres  10987  resqrexlem1arp  11007  maxabslemval  11210  xrmaxiflemval  11251  xrmaxadd  11262  xrminmax  11266  summodclem3  11381  fsumsplit  11408  mertenslemub  11535  fprodsplit  11598  demoivreALT  11774  zsupcllemstep  11938  gcdsupex  11950  gcdsupcl  11951  gcdneg  11975  bezoutlemsup  12002  eucalginv  12048  eucalg  12051  odzdvds  12237  fldivp1  12338  prmunb  12352  enctlem  12425  ctiunctlemfo  12432  intopsn  12718  grpsubval  12851  mulgnndir  12943  iscnp4  13589  cnntr  13596  tx2cn  13641  hmeontr  13684  hmeores  13686  xmetres2  13750  metres2  13752  limccnp2cntop  14017  limccoap  14018  isomninnlem  14638  iswomninnlem  14657  ismkvnnlem  14660