Theorem adantlr 393

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
adantlr	|- (((ph /\ th) /\ ps) -> ch)

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 371	. . 3 |- (ph -> (ps -> ch))
3	2	adantr 389	. 2 |- ((ph /\ th) -> (ps -> ch))
4	3	imp 348	1 |- (((ph /\ th) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  ad2ant2r 409  ad2ant2rl 411  anabss5 505  3ad2antl1 815  3ad2antl2 816  3adant1r 859  ax11eq 1402  ax11el 1403  ax11indalem 1407  ax11inda2ALT 1408  tz7.7 3001  onmindif2 3169  peano5 3241  relop 3365  fvelimab 3876  ssimaex 3879  eqfnfv 3909  eqfnfv2 3911  fconst2g 3959  isocnv 4010  isotr 4011  isotrALT 4012  tfrlem2 4213  oaordi 4316  oawordri 4320  oaass 4331  omlimcl 4345  odi 4346  omass 4347  oeordi 4350  oewordri 4355  oeoe 4362  oaabs 4392  omsmolem 4396  omsmo 4397  xpdom2 4583  ac6sfilem3 4590  sbthlem9 4600  mapenlem1 4636  mapenlem2 4637  mapxpen 4642  xpmapenlem3 4645  xpmapenlem4 4646  fiint 4703  fodomfib 4710  noinfep 4786  aceq5 4886  ac6lem 4900  zorn2lem6 4939  zorn2lem7 4940  fodom 4944  unxpdomlem 4993  axrepndlem2 5099  axrepnd 5100  axpowndlem2 5104  axacndlem5 5117  axacnd 5118  mulcanpi 5181  indpi 5188  genpnmax 5264  addclprlem2 5273  mulclprlem 5275  prlem934b 5292  ssgt0sr 5371  cnegexlem1 5499  cnegexlem3 5501  cnegex 5502  1re 5589  axsup 5661  xrlttr 5707  rec11r 5918  divadddiv 5923  divdivdiv 5924  divcan6 5930  ltmul12a 5985  lemul12b 5986  lemul12aOLD 5987  ledivdiv 6035  lediv12a 6041  ledivp1 6050  nn2ge 6087  nnleltp1 6100  lbinfm 6216  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxrun 6253  supxrunb1 6257  supxrbnd 6259  zrevaddcl 6338  zltp1le 6349  zextle 6360  zbtwnre 6393  qreccl 6412  qrevaddcl 6414  irradd 6416  qbtwnre 6418  modadd1 6477  modmul1 6478  iooin 6498  elioc2 6516  elico2 6517  elicc2 6518  ioojoin 6543  uz11 6559  fzaddel 6630  fzrev 6642  fzrev3 6645  fsequb 6654  fsequb2 6655  ser1add2i 6703  expcllem 6770  expne0i 6782  mulexp 6788  exprec 6789  expadd 6791  expsub 6793  expdiv 6796  expmwordi 6803  expnlbnd 6853  expnlbnd2 6854  sqr2irrlem3 6927  seq1bndi 7113  cau2i 7116  caubndi 7129  sumeq2 7188  fsum1ps 7221  fsumsplit 7223  fsumcom 7231  fsummulc1 7236  fsumcmpndx2 7245  clm4lei 7284  2climnn 7305  2climnn0 7306  climrecl 7313  climaddlem3 7319  climmullem3 7325  climmullem4 7326  climmullem5 7327  climmullem8 7330  climmulc2 7332  climcmpc1 7342  climsqueeze 7343  climsqueeze2 7344  climserzlei 7350  climsupi 7358  isum1p 7410  isumrecl 7414  explecnv 7438  cvgratlem2ALT 7453  cvgratlem1 7455  cvgratlem2 7456  cvgratlem5 7459  fsum0diag2 7464  fsum0diag4 7466  elcncf 7470  reeff1o 7634  infxpidmlem1 7764  infxpidmlem11 7774  infxpidmlem12 7775  infxp 7784  infmap2lem2 7792  basgen2 7851  clsval2 7895  elcls 7914  elcls3 7921  opnssneib 7939  neissex 7948  iscnp2 7971  iscncl 7980  cnconst 7990  dnsconst 7998  metxplem4 8043  bl2in 8053  ssblex 8066  metequiv 8091  metcnplem 8097  metcnp 8098  metcnp2 8099  metcnpi3 8103  metcnpi4 8104  metcni2 8106  metcnp3 8107  metcnss 8109  bl2ioo 8122  tgioolem 8125  lmconst 8145  lmnn 8146  iscau3 8149  iscauf 8150  iscau4 8151  causs 8166  lmle 8171  metelcls 8176  metcnp4lem2 8180  metcn4 8182  xplmi 8184  xpcn 8187  bopcnlem2 8193  iscms2lem5 8204  cmsss 8208  cncms 8209  bcthlem9 8218  bcthlem11 8220  bcthlem16 8225  bcthlem19 8228  bcthlem20 8229  bcthlem21 8230  bcthlem24 8233  bcthlem25 8234  bcthlem26 8235  bcthlem29 8238  grpidinvlem3 8263  grplcan 8292  isgrp2i 8293  nvmul0or 8519  vacnlem3 8584  vacnlem5 8586  nmcnilem 8591  sm1cnilem 8601  sspmval 8646  sspival 8651  sspimsval 8653  nvcnpi3 8676  nvcnpi4 8677  nmoub3i 8690  0lno 8705  blocnilem 8719  blocni 8720  sspph 8771  ubthlem3 8789  ubthlem5 8791  ubthlem8 8794  ubthlem10 8796  minveclem9 8813  minveclem27 8831  minveclem30 8834  minveclem31 8835  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  abssinper 8980  h2hcau 9124  hvmul0or 9169  hvaddsub4 9221  hhcms 9348  hhsscms 9426  chocunii 9448  occllem6 9454  projlem25 9486  projlem26 9487  projlem28 9489  shsel3 9555  shsel1 9561  spansncol 9767  pjspansn 9776  5oalem2 9878  5oalem4 9880  3oalem2 9886  eigposi 10042  hhlnoi 10106  nmopub2tALT 10113  unoplin 10124  nmfnleub2 10130  hmopadj2 10145  hmoplin 10146  kbpj 10160  nmcopexlem6 10235  lnopconi 10242  nmcfnexlem6 10264  lnfnconi 10269  nlelchi 10273  riesz3i 10274  cnlnadjlem6 10284  adjadd 10305  branmfn 10317  branmfnOLD 10318  bra11 10321  leop2 10337  leopadd 10345  leopmuli 10346  leoptri 10349  leopnmid 10351  nmopleid 10352  pjss2coi 10372  pjssdif1i 10383  pj3si 10416  pj3cor1i 10418  hstle 10438  cvcon3 10492  mdbr2 10504  dmdbr2 10511  mddmd2 10517  mdslmd2i 10538  csmdsymi 10542  superpos 10562  atordi 10593  atcvatlem 10594  irredlem1 10599  irredi 10603  mdsymlem1 10612  mdsymlem2 10613  mdsymlem3 10614  mdsymlem4 10615  mdsymlem5 10616  sumdmdii 10624  cdj3i 10650  twpar2 10773  toplat 10884  mapudiscn 11015  iintlem1 11155  elicc3 11410  ordiso 11426  ordtypelem6 11432  omsubsuc2 11439  infenomsub 11450  omsubinit 11451  opnregcld 11467  cldregopn 11468  cnpnei 11472  subcld 11480  hscptsscld 11491  comptoppr 11495  alexsublem3 11498  alexsublem4 11499  connsub 11502  cnconn 11503  conntoppr 11504  subtopmet 11506  reconnlem1 11507  topfneec 11562  neibastop2lem3 11582  neibastop3 11585  topjoin 11588  fnemeet2 11590  fnejoin2 11592  isnrm2 11613  isufil2 11650  filssufil 11656  ufileulem 11657  uffixfr 11660  ufilen 11664  limfilcf 11683  cnpfillim 11686  elfilmap3 11692  rnelfmlem 11698  fmfnfmlem1 11700  fmfnfmlem4 11703  flimfcnp 11714  isfclus 11718  fclusnei 11719  fcluscf 11724  fcluscnplem 11729  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  ssga 11777  upixp 11823  indexd 11846  indexf 11847  filbcmb 11857  sdclem1 11875  sdclem2 11876  sdc 11877  incsequz 11879  nnubfi 11881  nninfnub 11882  fsumlt1 11894  metf1o 11907  blssp 11908  blhalf 11911  mettrifi 11912  geomcau 11914  caushft 11916  metdcn 11918  iccsplit 11919  iccshftr 11922  iccshftl 11924  iccdil 11926  icccntr 11928  iocopnst 11941  lincmb01cmp 11942  lincmb01icc 11943  cnimass 11949  cnres 11950  paste 11954  tlmconst 11968  lmtlm 11969  txbas 11973  tx1cn 11976  txcn 11979  txsubsp 11983  sstotbnd 11992  totbndss 11993  bndss 11998  totbndbnd 12000  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem16 12026  heiborlem23 12033  heiborlem28 12038  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  heiborlem36 12046  bfplem8 12061  bfplem9 12062  rrndstprj 12073  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  iccbnd 12082  phtpycom 12092  phtpyco 12098

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

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain