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  4420  fimacnvdisj  5442  fvimacnv  5677  ssct  6877  f1vrnfibi  7011  inl11  7131  ctssdc  7179  enomnilem  7204  enmkvlem  7227  djuen  7278  cauappcvgprlemlol  7714  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemlol  7737  caucvgprlemladdrl  7745  caucvgprprlemlol  7765  suplocsrlem  7875  recgt1i  8925  avgle2  9233  xnn0le2is012  9941  ioodisj  10068  fzneuz  10176  zsupcllemstep  10319  fihashfn  10892  shftfvalg  10983  shftfval  10986  cvg1nlemres  11150  resqrexlem1arp  11170  maxabslemval  11373  xrmaxiflemval  11415  xrmaxadd  11426  xrminmax  11430  summodclem3  11545  fsumsplit  11572  mertenslemub  11699  fprodsplit  11762  demoivreALT  11939  bitsp1  12115  gcdneg  12149  bezoutlemsup  12176  eucalginv  12224  eucalg  12227  odzdvds  12414  pclemdc  12457  fldivp1  12517  prmunb  12531  enctlem  12649  ctiunctlemfo  12656  intopsn  13010  grpsubval  13178  mulgnndir  13281  gsumfzreidx  13467  gsumfzmptfidmadd  13469  znunit  14215  iscnp4  14454  cnntr  14461  tx2cn  14506  hmeontr  14549  hmeores  14551  xmetres2  14615  metres2  14617  limccnp2cntop  14913  limccoap  14914  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696