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  4488  fimacnvdisj  5529  fvimacnv  5771  ssct  7043  f1vrnfibi  7187  inl11  7324  ctssdc  7372  enomnilem  7397  enmkvlem  7420  djuen  7486  cauappcvgprlemlol  7927  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgprlemlol  7950  caucvgprlemladdrl  7958  caucvgprprlemlol  7978  suplocsrlem  8088  recgt1i  9137  avgle2  9445  eluzmn  9823  xnn0le2is012  10162  ioodisj  10289  fzneuz  10398  zsupcllemstep  10552  fihashfn  11126  shftfvalg  11458  shftfval  11461  cvg1nlemres  11625  resqrexlem1arp  11645  maxabslemval  11848  xrmaxiflemval  11890  xrmaxadd  11901  xrminmax  11905  summodclem3  12021  fsumsplit  12048  mertenslemub  12175  fprodsplit  12238  demoivreALT  12415  bitsp1  12592  gcdneg  12633  bezoutlemsup  12660  eucalginv  12708  eucalg  12711  odzdvds  12898  pclemdc  12941  fldivp1  13001  prmunb  13015  enctlem  13133  ctiunctlemfo  13140  pwssnf1o  13461  intopsn  13530  grpsubval  13709  mulgnndir  13818  gsumfzreidx  14004  gsumfzmptfidmadd  14006  znunit  14755  iscnp4  15029  cnntr  15036  tx2cn  15081  hmeontr  15124  hmeores  15126  xmetres2  15190  metres2  15192  limccnp2cntop  15488  limccoap  15489  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785  gfsumval  16809