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  5886  funfvima3  5887  foco2  5893  isores3  5955  oprabid  6049  ovmpt4g  6143  ovmpos  6144  ov2gf  6145  ovmpodf  6152  suppssfv  6230  suppssov1  6231  fo2ndf  6391  rntpos  6422  tposf2  6433  nnmordi  6683  nnmord  6684  nnaordex  6695  ectocld  6769  qsel  6780  mapsn  6858  f1oeng  6929  mapen  7031  nneneq  7042  findcard2  7077  findcard2s  7078  ac6sfi  7086  fiintim  7122  sbthlem1  7155  pr2ne  7396  ltbtwnnqq  7634  prnmaddl  7709  genpcdl  7738  genpcuu  7739  ltaddpr  7816  lteupri  7836  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemdisj  7870  lttrsr  7981  recexgt0sr  7992  mulgt0sr  7997  axprecex  8099  rereceu  8108  addlsub  8548  recexap  8832  0mnnnnn0  9433  prime  9578  zeo  9584  fnn0ind  9595  zindd  9597  btwnz  9598  lbzbi  9849  addmodlteq  10659  facwordi  11001  seq3coll  11105  ccatalpha  11189  pfxccatin12lem2a  11307  qdenre  11762  climcau  11907  serf0  11912  zsumdc  11944  fsum2dlemstep  11994  fsum2d  11995  fsumabs  12025  fsumiun  12037  zproddc  12139  fprod2dlemstep  12182  fprod2d  12183  odd2np1  12433  ndvdssub  12490  bitsinv1lem  12521  dfgcd2  12584  nprm  12694  rpexp  12724  pc2dvds  12902  pcfac  12922  4sqlem12  12974  4sqlem17  12979  divsfval  13410  mulgaddcom  13732  mulginvcom  13733  ringinvnz1ne0  14061  lmss  14969  lmtopcnp  14973  txcn  14998  txlm  15002  xmettri2  15084  blin2  15155  metcnp3  15234  limcresi  15389  dvmptfsum  15448  logbgcd1irr  15690  lgsdir2lem2  15757  lgsne0  15766  2lgsoddprm  15841  2sqlem6  15848  2sqlem10  15853  uhgr0vb  15934  wlk1walkdom  16209  wlkv0  16219  wlklenvclwlk  16223  bj-stim  16342  bj-stan  16343  bj-stand  16344  bj-stal  16345  bj-sbimedh  16367  bj-vtoclgft  16371  elabgft1  16374  elabgf2  16376