Theorem adantlr 402

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 380	. . 3 |- (ph -> (ps -> ch))
3	2	adantr 398	. 2 |- ((ph /\ th) -> (ps -> ch))
4	3	imp 357	1 |- (((ph /\ th) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  ad2ant2r 418  ad2ant2rl 420  anabss5 513  3ad2antl1 821  3ad2antl2 822  3adant1r 865  ax11eq 1405  ax11el 1406  ax11indalem 1410  ax11inda2ALT 1411  tz7.7 3030  onmindif2 3118  peano5 3210  relop 3332  fvelimab 3822  ssimaex 3825  eqfnfv 3854  fconst2g 3902  isocnv 3954  isotr 3955  isotrALT 3956  tfrlem2 3970  oaordi 4238  oawordri 4242  oaass 4253  omlimcl 4267  odi 4268  omass 4269  oeordi 4272  oewordri 4277  oaabs 4310  omsmolem 4314  omsmo 4315  xpdom2 4505  sbthlem9 4518  mapenlem1 4554  mapenlem2 4555  mapxpen 4560  xpmapenlem3 4563  xpmapenlem4 4564  fiint 4620  fodomfib 4627  noinfep 4702  aceq5 4802  ac6lem 4816  zorn2lem6 4855  zorn2lem7 4856  fodom 4860  unxpdomlem 4908  axrepndlem2 5010  axrepnd 5011  axpowndlem2 5015  axacndlem5 5028  axacnd 5029  mulcanpi 5092  indpi 5099  genpnmax 5175  addclprlem2 5184  mulclprlem 5186  prlem934b 5203  ssgt0sr 5282  cnegexlem1 5410  cnegexlem3 5412  cnegex 5413  1re 5500  axsup 5572  xrlttr 5618  divadddiv 5842  divcan6 5849  ltmul12a 5899  lemul12b 5900  lemul12aOLD 5901  lemuldivOLD 5935  ledivdiv 5950  lediv12a 5956  ledivp1 5965  nn2ge 6002  nnleltp1 6015  lbinfm 6130  xrsupsslem 6158  xrinfmsslem 6159  xrub 6162  supxrun 6167  supxrunb1 6171  supxrbnd 6173  zrevaddcl 6252  zltp1le 6263  zextle 6274  zbtwnre 6306  qreccl 6325  qrevaddcl 6327  irradd 6329  qbtwnre 6331  modadd1 6380  iooin 6397  elioc2 6415  elico2 6416  elicc2 6417  ioojoin 6442  uz11 6458  fzaddel 6526  fzrev 6537  fzrev3 6540  fsequb 6549  fsequb2 6550  ser1add2i 6597  expcllem 6664  mulexp 6683  expadd 6685  divexp 6688  expmwordi 6695  expnlbnd 6744  expnlbnd2 6745  sqr2irrlem3 6816  seq1bndi 7000  cau2i 7003  caubndi 7016  sumeq2 7075  fsum1ps 7108  fsumspl 7110  fsumcom 7118  fsummulc1 7123  fsumcmpndx2 7132  clm4lei 7171  2climnni 7192  2climnn0i 7193  climrecl 7200  climaddlem3 7206  climmullem3 7212  climmullem4 7213  climmullem5 7214  climmullem8 7217  climmulc2 7219  climcmpc1 7229  climsqueeze 7230  climsqueeze2 7231  climserzlei 7237  climsupi 7245  isum1p 7296  isumrecl 7300  cvgratlem2ALT 7338  cvgratlem1 7340  cvgratlem2 7341  cvgratlem5 7344  fsum0diag2 7349  fsum0diag4 7351  elcncf 7355  reeff1o 7517  infxpidmlem1 7644  infxpidmlem11 7654  infxpidmlem12 7655  infxp 7664  infmap2lem2 7672  basgen2 7728  clsval2 7770  elcls 7789  elcls3 7796  opnssneib 7814  neissex 7823  iscnp2 7846  iscncl 7855  cnconst 7865  dnsconst 7873  metxplem4 7918  bl2in 7928  ssblex 7941  metcnplem 7971  metcnp 7972  metcnp2 7973  metcnpi3 7977  metcnpi4 7978  metcni2 7980  metcnp3 7981  metcnss 7983  bl2ioo 7996  tgioolem 7999  lmconst 8019  lmnn 8020  iscau3 8023  iscauf 8024  iscau4 8025  causs 8040  lmle 8045  metelcls 8050  metcnp4lem2 8054  metcn4 8056  xplmi 8058  xpcn 8061  bopcnlem2 8067  iscms2lem5 8078  cmsss 8082  cncms 8083  bcthlem9 8092  bcthlem11 8094  bcthlem16 8099  bcthlem19 8102  bcthlem20 8103  bcthlem21 8104  bcthlem24 8107  bcthlem25 8108  bcthlem26 8109  bcthlem29 8112  grpidinvlem3 8135  grplcan 8159  isgrp2i 8160  nvmul0or 8356  nmcnilem 8421  sm1cnilem 8431  sspmval 8476  sspival 8481  sspimsval 8483  nvcnpi3 8506  nvcnpi4 8507  nmoub3i 8520  0lno 8534  blocnilem 8548  blocni 8549  sspph 8599  ubthlem3 8615  ubthlem5 8617  ubthlem8 8620  ubthlem10 8622  minveclem9 8637  minveclem27 8655  minveclem30 8658  minveclem31 8659  spwpr4OLD 8746  spwpr4aOLD 8747  abssinper 8795  h2hcau 8932  hvmul0or 8977  hvaddsub4 9028  hhcms 9155  hhsscms 9233  chocunii 9255  occllem6 9261  projlem25 9293  projlem26 9294  projlem28 9296  shsel3 9362  shsel1 9368  spansncol 9574  pjspansn 9583  5oalem2 9683  5oalem4 9685  3oalem2 9691  eigposi 9845  hhlnoi 9909  nmopub2tALT 9916  unoplin 9927  nmfnleub2 9933  hmopadj2 9948  hmoplin 9949  kbpj 9963  eighmorth 9971  nmcopexlem6 10039  lnopconi 10046  nmcfnexlem6 10068  lnfnconi 10073  nlelchi 10077  riesz3i 10078  cnlnadjlem6 10088  adjadd 10109  branmfn 10121  bra11 10124  leop2 10140  leopadd 10148  leopmuli 10149  leoptri 10152  leopnmid 10154  nmopleid 10155  pjss2coi 10175  pjssdif1i 10186  pj3si 10219  pj3cor1i 10221  hstle 10241  cvcon3 10295  mdbr2 10307  dmdbr2 10314  mddmd2 10320  mdslmd2i 10341  csmdsymi 10345  superpos 10365  atordi 10395  atcvatlem 10396  irredlem1 10401  irredi 10405  mdsymlem1 10414  mdsymlem2 10415  mdsymlem3 10416  mdsymlem4 10417  mdsymlem5 10418  sumdmdii 10426  cdj3i 10452  twpar2 10567  mapudiscn 10606  iintlem1 10714

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 154  df-an 232

Copyright terms: Public domain