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 391  sylan2 451  pm2.36 568  pm5.18 658  elimant 682  prlem1 768  syl3an2 858  meredith 921  ax4 969  ax5o 971  ax5 973  a4sd 982  hbnt 999  19.21 1052  equtr2 1129  hbae 1141  dvelimfALT 1149  cbv2 1159  sbied 1191  ax11a2 1211  sb4 1218  hbsb4 1243  ax11v 1260  ax11indn 1359  ax11inda2 1363  a12study 1371  hbeu 1382  euimmo 1413  mopick 1426  moeq3 1912  sbcbid 1966  sbc19.20dv 1975  ra4sbc 1987  csbexg 1998  csbeq2d 2008  pwssun 2816  reuuni4 2877  ralxfr 2889  wereu 2935  tz7.7 2963  onfr 2976  ordtr2 2992  ordunidif 2995  onint 2996  trsucss 3046  suc11 3083  limuni3 3113  tfi 3116  tfis 3117  limomss 3127  ordom 3131  peano5 3143  tfinds 3151  vtoclrbr 3202  relssres 3376  cores 3485  funss 3520  funopg 3533  imadif 3560  fneu 3578  fco 3621  rnssopab 3810  fconst5 3833  funfvima2 3838  funfvima3 3839  tfrlem1 3896  tfrlem5 3900  tfrlem11 3906  tz7.48lem 3940  tz7.48-1 3941  tz7.49 3944  tz7.49c 3945  omordi 4181  omord 4183  omass 4195  oneo 4196  oewordri 4203  oeworde 4204  omsmolem 4240  omsmo 4241  mapsn 4329  ssdomg 4389  sbthlem1 4427  fodomr 4463  pwuninelg 4467  nneneq 4492  php 4493  infsdomnn 4511  pssnn 4513  unblem1 4517  unblem2 4518  unbnn2 4522  isfinite2 4523  fiint 4534  fodomfi 4540  supub 4554  suplub 4555  sucprcreg 4572  inf3lem2 4586  inf3lem3 4587  infensuc 4610  noinfep 4612  trcl 4617  zfregs 4619  rankr1 4646  rankuni2 4662  hta 4700  aceq5 4712  kmlem4 4740  kmlem11 4747  kmlem12 4748  weth 4759  zorn2lem5 4764  zorn2lem6 4765  carddom 4808  sucdom 4814  ondomcard 4829  carduni 4830  alephordi 4846  cardaleph 4857  carduniima 4862  alephval2 4874  alephval3 4875  cfsuc 4887  axpowndlem3 4923  axregndlem1 4926  axregnd 4928  axacndlem1 4931  axacndlem2 4932  axacndlem3 4933  axacndlem4 4934  axacnd 4936  indpi 5006  ltrpq 5057  genpcd 5081  prlem934 5111  ltaddpr 5112  ltexprlem1 5114  ltexprlem2 5115  ltexprlem7 5120  ltaprlem 5122  ltapr 5123  prlem936 5127  reclem2pr 5129  reclem3pr 5130  reclem4pr 5131  mulcmpblnr 5155  recexsrlem 5184  mulgt0sr 5186  recexsr 5188  suppsr2 5195  pre-axsup 5263  addsubt 5356  1re 5407  recext 5657  nnleltp1t 5901  infmsup 6015  nnunb 6017  xrub 6027  primet 6142  zeot 6146  dfuz 6150  btwnz 6163  qbtwnre 6216  seq1rn2 6258  uz11t 6364  elfzlem 6405  fsequb 6455  seqzrn2 6488  creur 6673  creui 6674  cvg3 6860  facwordit 6881  fsum1 6943  fsumshftm 6970  serzcl2t 6987  2climnn 7039  2climnn0 7040  clim2serzt 7070  iserzmulc1 7072  climserzle 7083  caucvglem6 7098  isum1p 7141  isummulc1ALT 7148  fsum0diaglem2 7192  abscncflem 7209  unbenlem 7447  infxpidmlem10 7504  infxpidmlem11 7505  infmap2lem1 7521  tgss2t 7579  basgen2t 7581  bastop 7584  subbas2 7587  qdensere 7691  cnconst 7719  hausnei 7723  mettri2 7752  mettri4 7753  opnin 7809  metcni 7833  metcn4i 7906  xplmi 7907  xplm 7909  xpcn 7910  iscms2lem4 7926  lmcau 7930  isgrp 7975  grpidinvlem3 7984  ringdi 8083  ringdir 8084  ringass 8085  vcdi 8108  vcdir 8109  vcass 8110  nvex 8169  nvs 8229  nvtri 8237  lnolin 8349  efifolem4 8640  hlimunii 9029  chsscm 9033  chocuni 9088  occllem6 9094  occl 9097  projlem28 9129  pjthlem12 9145  chintcl 9210  chlejb1 9314  elspansn4t 9413  osumlem4 9498  spansncv 9514  hoaddsubt 9659  lnoplt 9754  lnfnlt 9771  nmcopexlem6 9871  lnopcon 9878  nmcfnexlem6 9900  lnfncon 9905  nlelch 9909  riesz4 9911  rnbra 9953  bra11 9954  pjnormss 10007  pj3s 10045  stle 10077  stcltr2 10112  dmdmdt 10137  mdslmd1lem2 10161  atssmat 10213  atcvatlem 10220  irredlem1 10225  atcvat4 10232  mdsymlem2 10239  mdsymlem6 10243  sumdmdlem2 10253  dmdbr5at 10255  cdjreu 10264  ghomf1olem 10301  oooeqim2 10371  cdrci 10381  cmphmp 10408  hmeogrp 10425  fipfil2 10439  filintf 10443  iintlem1 10476  eqidob 10567  cmpassoh 10573  homgrf 10574  cmpmon 10585  idmon 10588

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

Copyright terms: Public domain