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 120  syl5ib 204  syl5ibr 205  syl5bi 206  syl5bir 208  jao 338  adantrd 391  sylan2 453  pm2.36 573  pm5.18 663  elimant 688  prlem1 775  syl3an2 866  meredith 931  ax4 1008  ax5o 1010  ax5 1012  a4sd 1021  hbnt 1038  19.21 1092  equtr2 1170  hbae 1182  dvelimfALT 1190  cbv2 1200  sbied 1232  ax11a2 1253  sb4 1260  hbsb4 1286  ax11v 1303  ax11indn 1405  ax11inda2 1409  a12study 1417  hbeu 1428  euimmo 1459  mopick 1472  moeq3 1967  sbcbid 2024  sbc19.20dv 2033  ra4sbc 2047  csbexg 2059  csbeq2d 2069  pwssun 2905  wereu 2972  tz7.7 3001  onfr 3014  ordtr2 3019  ordunidif 3022  trsucss 3057  suc11 3073  reuuni4 3110  ralxfr 3122  onint 3152  limuni3 3206  tfi 3207  tfis 3208  tfinds 3212  limomss 3224  ordom 3228  peano5 3241  vtoclrbr 3295  opelxpex2 3369  relssres 3482  cores 3602  funss 3639  funopg 3652  imadif 3679  fneu 3698  fco 3743  rnssopab 3939  fconst5 3962  funfvima2 3967  funfvima3 3968  onfununi 4209  tfrlem1 4212  tfrlem5 4216  tfrlem11 4222  tz7.48lem 4256  tz7.48-1 4257  tz7.49 4260  tz7.49c 4261  omordi 4333  omord 4335  omass 4347  oneo 4348  oewordri 4355  oeworde 4356  omsmolem 4396  omsmo 4397  mapsn 4486  ssdomg 4549  ac6sfilem3 4590  ac6sfi 4591  sbthlem1 4592  fodomr 4628  pwuninel 4631  2pwuninel 4632  nneneq 4659  php 4660  infsdomnn 4678  pssnn 4681  unblem1 4686  unblem2 4687  unbnn2 4691  isfinite2 4692  fiint 4703  fodomfi 4709  supub 4723  suplub 4724  sucprcreg 4743  inf3lem2 4759  inf3lem3 4760  infensuc 4784  noinfep 4786  trcl 4791  zfregs 4793  rankr1 4820  rankuni2 4836  hta 4874  aceq5 4886  kmlem4 4914  kmlem11 4921  kmlem12 4922  weth 4933  zorn2lem5 4938  zorn2lem6 4939  carddom 4985  sucdom 4992  ondomcard 5007  carduni 5008  alephordi 5024  cardaleph 5035  carduniima 5040  alephval2 5052  alephval3 5053  cfsuc 5065  axpowndlem3 5105  axregndlem1 5108  axregnd 5110  axacndlem1 5113  axacndlem2 5114  axacndlem3 5115  axacndlem4 5116  axacnd 5118  indpi 5188  ltrpq 5239  genpcd 5263  prlem934 5293  ltaddpr 5294  ltexprlem1 5296  ltexprlem2 5297  ltexprlem7 5302  ltaprlem 5304  ltapr 5305  prlem936 5309  reclem2pr 5311  reclem3pr 5312  reclem4pr 5313  mulcmpblnr 5337  recexsrlem 5366  mulgt0sr 5368  recexsr 5370  suppsr2 5377  pre-axsup 5445  addsub 5538  1re 5589  recex 5840  nnleltp1 6100  infmsup 6236  nnunb 6238  xrub 6248  prime 6366  zeo 6370  dfuzi 6373  btwnz 6387  qbtwnre 6418  uz11 6559  elfzlem 6601  fsequb 6654  seq1rn2 6686  seqzrn2 6751  creur 6943  creui 6944  cvg3i 7126  facwordi 7147  fsum1i 7208  fsumshftm 7235  serzcl2 7252  2climnn 7305  2climnn0 7306  clim2serz 7337  iserzmulc1 7339  climserzlei 7350  caucvglem6 7365  isum1p 7410  isummulc1iALT 7417  fsum0diaglem2 7462  abscncflem 7479  unbenlem 7716  infxpidmlem10 7773  infxpidmlem11 7774  infmap2lem1 7791  tgss2 7849  basgen2 7851  bastop1 7854  subbas2 7857  qdensere 7961  cnconst 7990  hausnei 7994  mettri2 8023  mettri4 8024  opnin 8079  metcni 8105  metcn4i 8183  xplmi 8184  xplm 8186  xpcn 8187  iscms2lem4 8203  lmcau 8207  isgrp 8254  grpidinvlem3 8263  gxcom 8325  gxinv 8326  gxid 8329  gxdi 8355  ringideu 8387  ringdi 8388  ringdir 8389  ringass 8390  vcdi 8418  vcdir 8419  vcass 8420  nvex 8477  nvs 8537  nvtri 8545  vacnlem6 8587  lnolin 8669  sineq0re 8985  efifolem4 8997  hlimuniii 9384  chsscmi 9388  chocunii 9448  occllem6 9454  occli 9457  projlem28 9489  pjthlem12 9506  chintcli 9571  chlejb1i 9675  elspansn4 9772  osumlem4 9859  spansncvi 9875  hoaddsub 10022  lnopl 10118  lnfnl 10135  nmcopexlem6 10235  lnopconi 10242  nmcfnexlem6 10264  lnfnconi 10269  nlelchi 10273  riesz4i 10275  rnbra 10320  bra11 10321  pjnormssi 10376  pj3si 10416  stlei 10448  stcltr2i 10483  dmdmd 10508  dmdbr5 10516  mdslmd1lem2 10534  atssma 10587  atcvatlem 10594  irredlem1 10599  atcvat4i 10606  mdsymlem2 10613  mdsymlem6 10617  sumdmdlem2 10628  dmdbr5ati 10631  cdjreui 10641  xfree 10653  ghomf1olem 10681  oooeqim2 10759  ref3w 10772  sqpeq 10786  unpde2eg22 10826  dupos2 10879  tostos 10883  opidon 10898  rngmgmbs3 10944  rngmgmbs4 10945  rnplrnml3 10950  fldi 10974  cdrci 10994  cmphmp 11027  hmeogrp 11044  top2ind 11050  fipfil2 11077  filintf 11081  altretop 11144  iintlem1 11155  eqidob 11250  cmpassoh 11256  cmpmon 11270  idmon 11272  iepiclem 11278  finminlem 11418  inficlALT 11424  finsschain 11425  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  omsubel 11444  infenomsub 11450  omsubinit 11451  ntruni 11464  cnsubsp2 11484  compsub 11488  hscptsscld 11491  compfipin0lem 11492  cncomp 11494  comptoppr 11495  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  cnconn 11503  conntoppr 11504  reconnlem3 11509  reconnlem5 11511  2ndcctbss 11539  locfincomp 11575  neibastop2lem3 11582  topmtcl 11586  topjoin 11588  fbssint 11626  fbunfip 11631  fgfil 11638  fbfgss 11640  extbas1 11641  filfinnfr 11646  filufint 11659  ufilen 11664  filcon 11665  limfilcf 11683  cnpfillim 11686  elfilmap2 11691  fmfnfmlem1 11700  fcluscf 11724  flimfnfcls 11727  filnetlem5 11767  filnet 11768  findcard 11836  fixp 11840  indexf 11847  inficl 11849  filbcmb 11857  sdclem2 11876  seqpo 11878  nninfnub 11882  fsumlt1 11894  metsstop 11909  mettrifi2 11913  lmtlm 11969  tx1cn 11976  tx2cn 11977  totbndss 11993  totbndbnd 12000  ismtybndlem 12008  ismtyres 12010  heiborlem1 12011  heiborlem10 12020  heiborlem11 12021  heiborlem15 12025  heiborlem23 12033  heiborlem37 12047  heiborlem41 12051  rrntotbnd 12078

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

Copyright terms: Public domain