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  4476  fimacnvdisj  5510  fvimacnv  5750  ssct  6975  f1vrnfibi  7112  inl11  7232  ctssdc  7280  enomnilem  7305  enmkvlem  7328  djuen  7393  cauappcvgprlemlol  7834  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprlemlol  7857  caucvgprlemladdrl  7865  caucvgprprlemlol  7885  suplocsrlem  7995  recgt1i  9045  avgle2  9353  xnn0le2is012  10062  ioodisj  10189  fzneuz  10297  zsupcllemstep  10449  fihashfn  11022  shftfvalg  11329  shftfval  11332  cvg1nlemres  11496  resqrexlem1arp  11516  maxabslemval  11719  xrmaxiflemval  11761  xrmaxadd  11772  xrminmax  11776  summodclem3  11891  fsumsplit  11918  mertenslemub  12045  fprodsplit  12108  demoivreALT  12285  bitsp1  12462  gcdneg  12503  bezoutlemsup  12530  eucalginv  12578  eucalg  12581  odzdvds  12768  pclemdc  12811  fldivp1  12871  prmunb  12885  enctlem  13003  ctiunctlemfo  13010  pwssnf1o  13331  intopsn  13400  grpsubval  13579  mulgnndir  13688  gsumfzreidx  13874  gsumfzmptfidmadd  13876  znunit  14623  iscnp4  14892  cnntr  14899  tx2cn  14944  hmeontr  14987  hmeores  14989  xmetres2  15053  metres2  15055  limccnp2cntop  15351  limccoap  15352  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420