Theorem adantlr 429

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 402	. . 3 |- (ph -> (ps -> ch))
3	2	adantr 425	. 2 |- ((ph /\ th) -> (ps -> ch))
4	3	imp 377	1 |- (((ph /\ th) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  ad2ant2r 445  ad2ant2rl 447  anabss5 560  3ad2antl1 1038  3ad2antl2 1039  3adant1r 1091  ax11eq 1754  ax11el 1755  ax11indalem 1759  ax11inda2ALT 1760  tz7.7 3684  onmindif2 3893  peano5 3975  relop 4113  fvelimabOLD 4726  ssimaex 4729  eqfnfv 4766  fconst2g 4821  isocnv 4873  isotr 4874  isotrALT 4875  tfrlem2 5120  oaordi 5227  oawordri 5232  oaass 5243  omlimcl 5257  odi 5258  omass 5259  oeordi 5262  oewordri 5267  oeoe 5274  oaabs 5309  omsmolem 5313  omsmo 5314  xpdom2 5501  ac6sfilem3 5508  sbthlem9 5518  mapenlem1 5583  mapenlem2 5584  mapxpen 5589  xpmapenlem3 5592  xpmapenlem4 5593  fiint 5650  fodomfib 5657  ordiso 5683  ordtypelem6 5689  noinfep 5747  omsubsuc2 5878  infenomsub 5889  omsubinit 5890  aceq5 5902  ac6lem 5916  zorn2lem6 5955  zorn2lem7 5956  fodom 5960  unxpdomlem 5995  axrepndlem2 6097  axrepnd 6098  axpowndlem2 6102  axacndlem5 6115  axacnd 6116  mulcanpi 6179  indpi 6186  genpnmax 6262  addclprlem2 6271  mulclprlem 6273  prlem934b 6290  ssgt0sr 6369  cnegexlem1 6499  cnegexlem3 6501  cnegex 6502  1re 6598  axsup 6676  xrlttr 6728  rec11r 6955  divadddiv 6960  divdivdivOLD 6962  divcan6 6968  ltmul12a 7023  lemul12b 7024  lemul12aOLD 7025  ledivdiv 7073  lediv12a 7079  ledivp1 7088  nn2ge 7125  nnleltp1 7138  lbinfm 7257  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxrun 7294  supxrunb1 7298  supxrbnd 7300  zrevaddcl 7379  zltp1le 7390  zextle 7401  zbtwnre 7434  qreccl 7453  qrevaddcl 7455  irradd 7457  qbtwnre 7459  modadd1 7518  modmul1 7519  iooin 7539  elioc2 7558  elico2 7559  elicc2 7560  ioojoin 7585  uz11 7601  fzaddel 7672  fzrev 7689  fzrev3 7692  fsequb 7702  fsequb2 7703  ser1add2i 7751  expcllem 7818  expne0i 7830  mulexp 7836  exprec 7837  expadd 7839  expsub 7841  expdiv 7844  expmwordi 7851  expnlbnd 7902  expnlbnd2 7903  sqr2irrlem3 7976  seq1bndi 8162  cau2i 8165  caubndi 8178  sumeq2 8245  fsum1ps 8278  fsumsplit 8280  fsumcom 8288  fsummulc1 8293  fsumcmpndx2 8302  clm4lei 8341  2climnn 8362  2climnn0 8363  climrecl 8370  climaddlem3 8376  climmullem3 8382  climmullem4 8383  climmullem5 8384  climmullem8 8387  climmulc2 8389  climcmpc1 8399  climsqueeze 8400  climsqueeze2 8401  climserzlei 8407  climsupi 8415  isum1p 8467  isumrecl 8471  explecnv 8495  cvgratlem2ALT 8510  cvgratlem1 8512  cvgratlem2 8513  cvgratlem5 8516  fsum0diag2 8521  fsum0diag4 8523  elcncf 8527  reeff1o 8691  infxpidmlem1 8821  infxpidmlem11 8831  infxpidmlem12 8832  infxp 8841  infmap2lem2 8849  basgen2 8909  txbas 8933  clsval2 8961  elcls 8980  elcls3 8987  opnssneib 9005  neissex 9014  iscnp2 9037  cnpnei 9043  iscncl 9047  cnconst 9057  dnsconst 9065  metxplem4 9110  bl2in 9120  ssblex 9133  metequiv 9158  metcnplem 9164  metcnp 9165  metcnp2 9166  metcnpi3 9170  metcnpi4 9171  metcni2 9173  metcnp3 9174  metcnss 9176  bl2ioo 9189  tgioolem 9192  lmconst 9212  lmnn 9213  iscau3 9216  iscauf 9217  iscau4 9218  causs 9233  lmle 9238  metelcls 9243  metcnp4lem2 9247  metcn4 9249  xplmi 9251  xpcn 9254  bopcnlem2 9260  iscms2lem5 9271  cmsss 9275  cncms 9276  bcthlem9 9285  bcthlem11 9287  bcthlem16 9292  bcthlem19 9295  bcthlem20 9296  bcthlem21 9297  bcthlem24 9300  bcthlem25 9301  bcthlem26 9302  bcthlem29 9305  grpidinvlem3 9330  grplcan 9359  isgrp2i 9360  ssga 9455  nvmul0or 9604  vacnlem3 9669  vacnlem5 9671  nmcnilem 9676  sm1cnilem 9686  sspmval 9731  sspival 9736  sspimsval 9738  nvcnpi3 9761  nvcnpi4 9762  nmoub3i 9775  0lno 9790  blocnilem 9804  blocni 9805  sspph 9856  ubthlem3 9874  ubthlem5 9876  ubthlem8 9879  ubthlem10 9881  minveclem9 9898  minveclem27 9916  minveclem30 9919  minveclem31 9920  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  abssinper 10062  twpar2 10149  indexfi 10174  tx1cn 10223  txcn 10227  subcld 10254  subtopmet 10256  elfilmap3 10314  comptoppr 10332  h2hcau 10481  hvmul0or 10526  hvaddsub4 10578  hhcms 10705  hhsscms 10783  chocunii 10805  occllem6 10811  projlem25 10843  projlem26 10844  projlem28 10846  shsel3 10912  shsel1 10918  spansncol 11124  pjspansn 11133  5oalem2 11235  5oalem4 11237  3oalem2 11243  eigposi 11399  hhlnoi 11463  nmopub2tALT 11470  unoplin 11481  nmfnleub2 11487  hmopadj2 11502  hmoplin 11503  kbpj 11517  eighmorth 11525  nmcopexlem6 11593  lnopconi 11600  nmcfnexlem6 11622  lnfnconi 11627  nlelchi 11631  riesz3i 11632  cnlnadjlem6 11642  adjadd 11663  branmfn 11675  branmfnOLD 11676  bra11 11679  leop2 11695  leopadd 11703  leopmuli 11704  leoptri 11707  leopnmid 11709  nmopleid 11710  opsqrlem1 11711  pjss2coi 11736  pjssdif1i 11747  pj3si 11780  pj3cor1i 11782  hstle 11802  cvcon3 11856  mdbr2 11868  dmdbr2 11875  mddmd2 11881  mdslmd2i 11902  csmdsymi 11906  superpos 11926  atordi 11956  atcvatlem 11957  irredlem1 11962  irredi 11966  mdsymlem1 11975  mdsymlem2 11976  mdsymlem3 11977  mdsymlem4 11978  mdsymlem5 11979  sumdmdii 11987  cdj3i 12013  bnj849 13318  fzind 13610  suprzcl 13658  negdvdsb 13671  dvdsnegb 13672  gcdcllem3 13720  fundmpss 13836  dfon2lem8 13856  tz6.26 13913  frxp 13951  poseq 13954  soseq 13955  wfrlem4 13960  sltval2 13997  nocvxminlem 14028  axfelem7 14037  axfelem8 14038  axfelem9 14039  axfelem10 14040  axfelem14 14044  inpreima5 14469  toplat 14638  prodeq2 14661  curgrpact 14735  trran2 14757  mapudiscn 14872  usptoplem 14917  istopx 14918  iintlem1 15010  elicc3 15362  ordisoOLD 15374  ordtypelem6OLD 15380  omsubsuc2OLD 15387  infenomsubOLD 15398  omsubinitOLD 15399  opnregcld 15415  cldregopn 15416  hscptsscld 15434  alexsublem3 15439  alexsublem4 15440  connsub 15443  cnconn 15444  conntoppr 15445  reconnlem1 15446  topfneec 15501  neibastop2lem3 15521  neibastop3 15524  topjoin 15527  fnemeet2 15529  fnejoin2 15531  isnrm2 15552  isufil2 15565  filssufil 15571  ufileulem 15572  uffixfr 15575  ufilen 15579  limfilcf 15587  cnpfillim 15589  rnelfmlem 15592  fmfnfmlem1 15594  fmfnfmlem4 15597  flimfcnp 15602  isfclus 15606  fclusnei 15607  fcluscf 15612  fcluscnplem 15617  filnetlem3 15642  filnetlem5 15644  eqfnun 15705  upixp 15729  indexdom 15754  indexfiOLD 15755  frfi 15771  pofun 15772  filbcmb 15776  addsubeq4 15778  fzadd2 15791  fzsplit 15792  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  fdc1 15813  incsequz 15815  nnubfi 15818  nninfnub 15819  fsumlt1 15831  metf1o 15843  blssp 15844  blhalf 15846  mettrifi 15847  geomcau 15849  caushft 15851  metdcn 15853  iccsplit 15854  iccshftr 15857  iccshftl 15859  iccdil 15861  icccntr 15863  iocopnst 15877  lincmb01cmp 15878  lincmb01icc 15879  oprpiece1res2 15881  cnimass 15888  cnres 15889  paste 15893  tlmconst 15907  lmtlm 15908  txsubsp 15912  txmet 15925  sstotbnd 15936  totbndss 15937  bndss 15942  totbndbnd 15944  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  ismtybndlem 15952  ismtyres 15954  heiborlem16 15970  heiborlem23 15977  heiborlem28 15982  heiborlem32 15986  heiborlem33 15987  heiborlem35 15989  heiborlem36 15990  bfplem8 16005  bfplem9 16006  rrndstprj1 16017  rrndstprj2 16018  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  iccbnd 16026  ghomco 16040  grpkerinj 16042  phtpycom 16050  phtpyco 16056  reparpht 16065  pcofval 16072  pcoloopf 16079  pcohtpylem3 16082  pcohtpy 16083  pcoass 16085  pi1gp 16095  isdivrng2 16111  rnghomco 16128  riscer 16142  idlsubcl 16171  keridl 16180  ispridl2 16186  igenval2 16214  isfldidl 16216  ispridlc 16218  pridlc3 16221  dmncan1 16224  atomnle 17016  hlatmstc 17047  grpidinvlem3NEW 17111  grplcanNEW 17134

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 164  df-an 242

Copyright terms: Public domain