Theorem syl5 21

Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise.

Hypotheses

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

Assertion

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

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. 2 |- (ph -> (ps -> ch))
2		syl5.2	. . 3 |- (th -> ps)
3	2	imim1i 16	. 2 |- ((ps -> ch) -> (th -> ch))
4	1, 3	syl 10	1 |- (ph -> (th -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.04 30  nsyli 121  syl5ib 206  syl5ibr 207  syl5bi 208  syl5bir 210  jao 340  adantrd 393  sylan2 453  pm2.36 572  pm5.18 662  elimant 686  prlem1 772  syl3an2 862  meredith 926  ax4 974  ax5o 976  ax5 978  a4sd 987  hbnt 1004  19.21 1058  equtr2 1135  hbae 1147  dvelimfALT 1155  cbv2 1165  sbied 1197  ax11a2 1218  sb4 1225  hbsb4 1250  ax11v 1267  ax11indn 1368  ax11inda2 1372  a12study 1380  hbeu 1391  euimmo 1422  mopick 1435  moeq3 1924  sbcbid 1980  sbc19.20dv 1989  ra4sbc 2001  csbexg 2012  csbeq2d 2022  pwssun 2834  reuuni4 2894  ralxfr 2906  wereu 2952  tz7.7 2980  onfr 2993  ordtr2 3009  ordunidif 3012  onint 3013  trsucss 3063  suc11 3100  limuni3 3130  tfi 3133  tfis 3134  limomss 3144  ordom 3148  peano5 3160  tfinds 3168  vtoclrbr 3219  opelxpex2 3286  relssres 3399  cores 3506  funss 3541  funopg 3554  imadif 3581  fneu 3599  fco 3643  rnssopab 3832  fconst5 3855  funfvima2 3860  funfvima3 3861  tfrlem1 3918  tfrlem5 3922  tfrlem11 3928  tz7.48lem 3962  tz7.48-1 3963  tz7.49 3966  tz7.49c 3967  omordi 4204  omord 4206  omass 4218  oneo 4219  oewordri 4226  oeworde 4227  omsmolem 4263  omsmo 4264  mapsn 4352  ssdomg 4415  sbthlem1 4454  fodomr 4490  pwuninel 4493  2pwuninel 4494  nneneq 4519  php 4520  infsdomnn 4543  pssnn 4546  unblem1 4553  unblem2 4554  unbnn2 4558  isfinite2 4559  isfinite2OLD 4560  fiint 4576  fiintOLD 4577  fodomfi 4582  fodomfiOLD 4583  supub 4596  suplub 4597  sucprcreg 4616  inf3lem2 4630  inf3lem3 4631  infensuc 4655  noinfep 4657  trcl 4662  zfregs 4664  rankr1 4691  rankuni2 4707  hta 4745  aceq5 4757  kmlem4 4785  kmlem11 4792  kmlem12 4793  weth 4804  zorn2lem5 4809  zorn2lem6 4810  carddom 4853  sucdom 4859  sucdomOLD 4860  ondomcard 4875  carduni 4876  alephordi 4892  cardaleph 4903  carduniima 4908  alephval2 4920  alephval3 4921  cfsuc 4934  axpowndlem3 4970  axregndlem1 4973  axregnd 4975  axacndlem1 4978  axacndlem2 4979  axacndlem3 4980  axacndlem4 4981  axacnd 4983  indpi 5053  ltrpq 5104  genpcd 5128  prlem934 5158  ltaddpr 5159  ltexprlem1 5161  ltexprlem2 5162  ltexprlem7 5167  ltaprlem 5169  ltapr 5170  prlem936 5174  reclem2pr 5176  reclem3pr 5177  reclem4pr 5178  mulcmpblnr 5202  recexsrlem 5231  mulgt0sr 5233  recexsr 5235  suppsr2 5242  pre-axsup 5310  addsubt 5403  1re 5454  recext 5703  nnleltp1t 5963  infmsup 6077  nnunb 6079  xrub 6089  primet 6204  zeot 6208  dfuz 6211  btwnz 6224  qbtwnre 6286  seq1rn2 6329  uz11t 6440  elfzlem 6481  fsequb 6531  seqzrn2 6564  creur 6750  creui 6751  cvg3 6930  facwordit 6951  fsum1 7012  fsumshftm 7039  serzcl2t 7056  2climnn 7109  2climnn0 7110  clim2serzt 7141  iserzmulc1 7143  climserzle 7154  caucvglem6 7169  isum1p 7213  isummulc1ALT 7220  fsum0diaglem2 7264  abscncflem 7281  unbenlem 7512  infxpidmlem10 7569  infxpidmlem11 7570  infmap2lem1 7588  tgss2t 7643  basgen2t 7645  bastop 7648  qdensere 7755  cnconst 7784  hausnei 7788  mettri2 7817  mettri4 7818  opnin 7873  metcni 7898  metcn4i 7976  xplmi 7977  xplm 7979  xpcn 7980  iscms2lem4 7996  lmcau 8000  isgrp 8045  grpidinvlem3 8054  ringdi 8149  ringdir 8150  ringass 8151  vcdi 8174  vcdir 8175  vcass 8176  nvex 8233  nvs 8293  nvtri 8301  lnolin 8418  efifolem4 8727  hlimunii 9110  chsscm 9114  chocuni 9174  occllem6 9180  occl 9183  projlem28 9215  pjthlem12 9232  chintcl 9297  chlejb1 9401  elspansn4t 9498  osumlem4 9583  spansncv 9599  hoaddsubt 9744  lnoplt 9840  lnfnlt 9857  nmcopexlem6 9958  lnopcon 9965  nmcfnexlem6 9987  lnfncon 9992  nlelch 9996  riesz4 9998  rnbra 10042  bra11 10043  pjnormss 10098  pj3s 10138  stle 10170  stcltr2 10205  dmdmdt 10230  dmdbr5 10238  mdslmd1lem2 10256  atssmat 10308  atcvatlem 10315  irredlem1 10320  atcvat4 10327  mdsymlem2 10334  mdsymlem6 10338  sumdmdlem2 10349  dmdbr5at 10352  cdjreu 10362  ghomf1olem 10399  oooeqim2 10473  cdrci 10488  cmphmp 10515  hmeogrp 10532  top2ind 10542  fipfil2 10558  filintf 10562  iintlem1 10611  eqidob 10702  cmpassoh 10708  cmpmon 10722  idmon 10724

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

Copyright terms: Public domain