Theorem syl5 32

Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

Ref	Expression
syl5.1	|- ( ph -> ps )
syl5.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 |- ( ph -> ps )
2		syl5.2	. . 3 |- ( ch -> ( ps -> th ) )
3	1, 2	syl5com 29	. 2 |- ( ph -> ( ch -> th ) )
4	3	com12 30	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl56  34  syl2im  38  imim12i  59  pm2.86d  100  biimtrid  152  biimtrrid  153  imbitrid  154  adantld  278  adantrd  279  impel  280  mpan9  281  nsyli  654  pm2.36  811  pm4.72  834  pm2.18dc  862  con1dc  863  jadc  870  pm2.521dcALT  877  con1biimdc  880  condandc  888  pm5.18dc  890  pm2.68dc  901  syl3an2  1307  syl2an23an  1335  xor3dc  1431  alrimdh  1527  spsd  1586  a5i  1591  19.21h  1605  hbnt  1701  hbae  1766  sbiedh  1835  exdistrfor  1848  sbcof2  1858  ax11a2  1869  ax11v  1875  sb4  1880  hbsb4t  2066  exmoeudc  2143  euimmo  2147  mopick  2158  r19.37  2685  spcimgft  2882  spcimegft  2884  rr19.28v  2946  mob2  2986  euind  2993  reuind  3011  sbeqalb  3088  triun  4200  csbexga  4217  copsexg  4336  trssord  4477  trsuc  4519  trsucss  4520  abnexg  4543  ralxfrd  4559  rexxfrd  4560  ralxfrALT  4564  sucprcreg  4647  nlimsucg  4664  tfis  4681  relssres  5051  issref  5119  dmsnopg  5208  dfco2a  5237  imadif  5410  fvelima  5697  mptfvex  5732  fvmptdf  5734  fvmptf  5739  funfvima2  5887  funfvima3  5888  foco2  5894  isores3  5956  oprabid  6050  ovmpt4g  6144  ovmpos  6145  ov2gf  6146  ovmpodf  6153  suppssfv  6231  suppssov1  6232  fo2ndf  6392  rntpos  6423  tposf2  6434  nnmordi  6684  nnmord  6685  nnaordex  6696  ectocld  6770  qsel  6781  mapsn  6859  f1oeng  6930  mapen  7032  nneneq  7043  findcard2  7078  findcard2s  7079  ac6sfi  7087  fiintim  7123  sbthlem1  7156  pr2ne  7397  ltbtwnnqq  7635  prnmaddl  7710  genpcdl  7739  genpcuu  7740  ltaddpr  7817  lteupri  7837  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemdisj  7871  lttrsr  7982  recexgt0sr  7993  mulgt0sr  7998  axprecex  8100  rereceu  8109  addlsub  8549  recexap  8833  0mnnnnn0  9434  prime  9579  zeo  9585  fnn0ind  9596  zindd  9598  btwnz  9599  lbzbi  9850  addmodlteq  10661  facwordi  11003  seq3coll  11107  ccatalpha  11194  pfxccatin12lem2a  11312  qdenre  11780  climcau  11925  serf0  11930  zsumdc  11963  fsum2dlemstep  12013  fsum2d  12014  fsumabs  12044  fsumiun  12056  zproddc  12158  fprod2dlemstep  12201  fprod2d  12202  odd2np1  12452  ndvdssub  12509  bitsinv1lem  12540  dfgcd2  12603  nprm  12713  rpexp  12743  pc2dvds  12921  pcfac  12941  4sqlem12  12993  4sqlem17  12998  divsfval  13429  mulgaddcom  13751  mulginvcom  13752  ringinvnz1ne0  14081  lmss  14989  lmtopcnp  14993  txcn  15018  txlm  15022  xmettri2  15104  blin2  15175  metcnp3  15254  limcresi  15409  dvmptfsum  15468  logbgcd1irr  15710  lgsdir2lem2  15777  lgsne0  15786  2lgsoddprm  15861  2sqlem6  15868  2sqlem10  15873  uhgr0vb  15954  wlk1walkdom  16229  wlkv0  16239  wlklenvclwlk  16243  bj-stim  16393  bj-stan  16394  bj-stand  16395  bj-stal  16396  bj-sbimedh  16418  bj-vtoclgft  16422  elabgft1  16425  elabgf2  16427