Theorem syl5 20

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 19	. 2 |- ((ps -> ch) -> (th -> ch))
4	1, 3	syl 12	1 |- (ph -> (th -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim12i 21  pm2.04 34  nsyli 136  jadOLD2 157  syl5ib 223  syl5ibr 224  syl5bi 225  syl5bir 227  jao 367  adantrd 427  sylan2 500  mpan9 521  pm2.36 629  pm5.18OLD 723  elimant 748  pm5.75 821  prlem1OLD 849  syl3an2 1131  meredithOLD 1201  ax4 1318  ax5o 1320  ax5 1322  a4sd 1331  hbnt 1349  19.21 1403  19.21ad 1406  19.33b 1444  equtr2OLD 1493  hbae 1505  dvelimfALT 1514  cbv2 1524  sbied 1563  sbiedOLD 1564  ax11a2 1586  sb4 1593  hbsb4 1620  hbsb4t 1621  ax11v 1642  ax11indn 1757  ax11inda2 1761  a12study 1769  hbeu 1782  euimmo 1816  mopick 1833  moeq3 2432  euind 2439  reuind 2450  sbcthdv 2459  sbeqalb 2503  sbcbid 2504  sbcimdv 2519  ra4sbc 2536  csbexg 2548  csbeq2d 2561  copsexg 3537  pwssun 3578  wereu 3654  tz7.7 3684  onfr 3702  ordtr2OLD 3709  ordunidif 3712  trsuc 3752  trsuc2 3754  trsucss 3755  suc11 3773  reuuni4 3813  eualeqhb 3824  euexeqOLD 3826  ralxfr 3839  onint 3876  limuni3 3936  tfi 3937  tfis 3938  tfinds 3942  tfindsOLD 3943  limomss 3956  ordomOLD 3961  peano5 3975  vtoclrbr 4033  vtoclrbrOLD 4034  opelxpex2OLD 4120  relssres 4248  asymref2 4310  dfco2a 4394  cores 4400  coresOLD 4401  funssOLD 4440  funeu 4444  funopg 4454  imadif 4493  fneuOLD 4518  fcoOLD 4574  fvelima 4723  dffv2 4734  rnssopab 4798  fconst5 4824  funfvima2 4829  funfvima3 4830  onfununi 5116  tfrlem1 5119  tfrlem5 5123  tfrlem11 5129  tz7.48lem 5164  tz7.48-1 5165  tz7.49 5168  tz7.49c 5169  omordi 5245  omord 5247  omass 5259  oneo 5260  oewordri 5267  oeworde 5268  omsmolem 5313  omsmo 5314  mapsn 5404  ssdomg 5467  ac6sfilem3 5508  ac6sfi 5509  sbthlem1 5510  fodomr 5547  pwuninel 5550  2pwuninel 5551  riotaxfrd 5581  nneneq 5606  php 5607  infsdomnn 5625  pssnn 5628  unblem1 5633  unblem2 5634  unbnn2 5638  isfinite2 5639  fiint 5650  fodomfi 5656  supub 5670  suplub 5671  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  sucprcreg 5703  inf3lem2 5720  inf3lem3 5721  infensuc 5745  noinfep 5747  trcl 5752  zfregs 5754  rankr1 5785  rankuni2 5801  hta 5858  omsubel 5883  infenomsub 5889  omsubinit 5890  aceq5 5902  kmlem4 5930  kmlem11 5937  kmlem12 5938  weth 5949  zorn2lem5 5954  zorn2lem6 5955  carddom 5987  sucdom 5994  ondomcard 6009  carduni 6010  alephordi 6022  cardaleph 6033  carduniima 6038  alephval2 6050  alephval3 6051  cfsuc 6063  axpowndlem3 6103  axregndlem1 6106  axregnd 6108  axacndlem1 6111  axacndlem2 6112  axacndlem3 6113  axacndlem4 6114  axacnd 6116  indpi 6186  ltrpq 6237  genpcd 6261  prlem934 6291  ltaddpr 6292  ltexprlem1 6294  ltexprlem2 6295  ltexprlem7 6300  ltaprlem 6302  ltapr 6303  prlem936 6307  reclem2pr 6309  reclem3pr 6310  reclem4pr 6311  mulcmpblnr 6335  recexsrlem 6364  mulgt0sr 6366  recexsr 6368  suppsr2 6375  pre-axsup 6444  addcani 6505  addsubOLD 6543  1re 6598  recex 6876  nnleltp1 7138  infmsup 7277  nnunb 7279  xrub 7289  prime 7407  zeo 7411  dfuzi 7414  btwnz 7428  qbtwnre 7459  uz11 7601  elfzlem 7643  fsequb 7702  seq1rn2 7734  seqzrn2 7799  creur 7992  creui 7993  cvg3i 8175  facwordi 8196  fsum1i 8265  fsumshftm 8292  serzcl2 8309  2climnn 8362  2climnn0 8363  clim2serz 8394  iserzmulc1 8396  climserzlei 8407  caucvglem6 8422  isum1p 8467  isummulc1iALT 8474  fsum0diaglem2 8519  abscncflem 8536  unbenlem 8773  infxpidmlem10 8830  infxpidmlem11 8831  infmap2lem1 8848  tgss2 8907  basgen2 8909  bastop1 8912  subbas2 8915  qdensere 9027  cnconst 9057  hausnei 9061  mettri2 9090  mettri4 9091  opnin 9146  metcni 9172  metcn4i 9250  xplmi 9251  xplm 9253  xpcn 9254  iscms2lem4 9270  lmcau 9274  isgrp 9321  grpidinvlem3 9330  gxcom 9392  gxinv 9393  gxid 9396  gxdi 9422  ringideu 9470  ringdi 9471  ringdir 9472  ringass 9473  vcdi 9503  vcdir 9504  vcass 9505  nvex 9562  nvs 9622  nvtri 9630  vacnlem6 9672  lnolin 9754  sineq0re 10067  efifolem4 10079  indexfi 10174  findcard 10178  findcardOLD 10179  fixp 10180  cdrci 10182  tx1cn 10223  tx2cn 10224  fipfil2 10272  filintf 10274  fbssint 10279  fbunfip 10282  fbfgss 10288  fgfil 10290  extbas1 10291  elfilmap2 10313  cncomp 10331  comptoppr 10332  opidon 10369  rngmgmbs4 10401  hlimuniii 10741  chsscmi 10745  chocunii 10805  occllem6 10811  occli 10814  projlem28 10846  pjthlem12 10863  chintcli 10928  chlejb1i 11032  elspansn4 11129  osumlem4 11216  spansncvi 11232  hoaddsub 11379  lnopl 11475  lnfnl 11492  nmcopexlem6 11593  lnopconi 11600  nmcfnexlem6 11622  lnfnconi 11627  nlelchi 11631  riesz4i 11633  rnbra 11678  bra11 11679  pjnormssi 11740  pj3si 11780  stlei 11812  stcltr2i 11847  dmdmd 11872  dmdbr5 11880  mdslmd1lem2 11898  atssma 11950  atcvatlem 11957  irredlem1 11962  atcvat4i 11969  mdsymlem2 11976  mdsymlem6 11980  sumdmdlem2 11991  dmdbr5ati 11994  cdjreui 12004  xfree 12016  bnj44 12419  bnj1110 13417  ghomf1olem 13637  lbzbi 13657  ndvdssub 13710  ndvdsadd 13711  gcdcllem3 13720  coprm 13782  trsuc2OLD 13793  fundmpss 13836  dfon2lem3 13851  dfon2lem4 13852  dfon2lem6 13854  dfon2lem8 13856  dfon2lem9 13857  hbntg 13872  tfisg 13912  wfisg 13917  trclss 13935  frinsg 13941  frxp 13951  soseq 13955  wfr3g 13956  wfrlem4 13960  wfrlem5 13961  frr3g 13980  sltval2 13997  axbday 14012  axdenselem5 14023  axfelem10 14040  axfelem11 14041  axfelem15 14045  axfelem16 14046  altopth1 14092  altopth2 14093  oooeqim2 14356  ref4w 14370  sqpeq 14383  surrc2 14390  unpde2eg22 14407  reflincror 14446  injrec 14461  fopab2g 14485  repcpwti 14503  unprj 14511  prl2 14514  domrancur1c 14550  valcurfn1 14552  dupos2 14587  dutos1 14626  tostos 14637  fprod1i 14673  rngmgmbs3 14766  rnplrnml3 14768  fldi 14776  rngridfz 14786  cmphmp 14878  hmeogrp 14892  top2ind 14897  topgrpbs 14974  altretop 14997  iintlem1 15010  eqidob 15144  cmpassoh 15150  cmpmon 15164  idmon 15166  iepiclem 15172  cptarc 15242  intartar 15255  finminlem 15367  inficlALT 15372  finsschain 15373  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  omsubelOLD 15392  infenomsubOLD 15398  omsubinitOLD 15399  ntruni 15412  cnsubsp2 15427  compsub 15431  hscptsscld 15434  compfipin0lem 15435  alexsublem3 15439  alexsublem4 15440  alexsub 15441  dfcon2 15442  cnconn 15444  conntoppr 15445  reconnlem3 15448  reconnlem5 15450  2ndcctbss 15478  locfincomp 15514  neibastop2lem3 15521  topmtcl 15525  topjoin 15527  filfinnfr 15561  filufint 15574  ufilen 15579  filcon 15580  limfilcf 15587  cnpfillim 15589  fmfnfmlem1 15594  fcluscf 15612  flimfnfcls 15615  filnetlem5 15644  filnet 15645  foco2 15686  enf1f1o 15720  findcard2 15745  fimax 15746  indexfiOLD 15755  inficl 15757  frfi 15771  filbcmb 15776  fzsplit 15792  sdclem2 15810  seqpo 15814  nninfnub 15819  fsumlt1 15831  mettrifi2 15848  lmtlm 15908  txmet 15925  totbndss 15937  totbndbnd 15944  ismtybndlem 15952  ismtyres 15954  heiborlem1 15955  heiborlem10 15964  heiborlem11 15965  heiborlem15 15969  heiborlem23 15977  heiborlem37 15991  heiborlem41 15995  rrntotbnd 16022  grpkerinj 16042  divrngidl 16176  prnc 16215  erdisj3 16266  prter2 16285  prter3 16286  pm11.71 16354  ax10ext 16364  cla4gft 16406  smores 16446  smoge 16454  e222 16526  e111 16564  e333 16601  atcvrj0 17065  grpidinvlem3NEW 17111  ringideuNEW 17146  pmaple 17241  paddasslem5 17285  osumcllem11 17374  pexmidlem8 17385

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

Copyright terms: Public domain