HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 adant2.1 . . . 4 |- ((ph /\ ps) -> ch)
21ex 373 . . 3 |- (ph -> (ps -> ch))
32adantr 389 . 2 |- ((ph /\ th) -> (ps -> ch))
43imp 350 1 |- (((ph /\ th) /\ ps) -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  ad2ant2r 409  ad2ant2rl 411  anabss5 501  3ad2antl1 807  3ad2antl2 808  3adant1r 851  ax11eq 1356  ax11el 1357  ax11indalem 1361  ax11inda2ALT 1362  tz7.7 2963  onmindif2 3051  peano5 3143  relop 3265  fvelimab 3750  ssimaex 3753  eqfnfv 3782  fconst2g 3830  isocnv 3881  isotr 3882  isotrALT 3883  tfrlem2 3897  oaordi 4164  oawordri 4168  oaass 4179  omlimcl 4193  odi 4194  omass 4195  oeordi 4198  oewordri 4203  oaabs 4236  omsmolem 4240  omsmo 4241  xpdom2 4422  sbthlem9 4435  mapenlem1 4469  mapenlem2 4470  mapxpen 4475  xpmapenlem3 4478  xpmapenlem4 4479  fiint 4534  fodomfib 4541  noinfep 4612  aceq5 4712  ac6lem 4726  zorn2lem6 4765  zorn2lem7 4766  fodom 4770  unxpdomlem 4815  axrepndlem2 4917  axrepnd 4918  axpowndlem2 4922  axacndlem5 4935  axacnd 4936  mulcanpi 4999  indpi 5006  genpnmax 5082  addclprlem2 5091  mulclprlem 5093  prlem934b 5110  ssgt0sr 5189  cnegextlem1 5317  cnegextlem3 5319  cnegext 5320  1re 5407  axsup 5479  xrlttrt 5526  divadddivt 5740  divcan6t 5747  ltmul12it 5797  lemul12ait 5798  lemul12itOLD 5799  lemuldivt 5824  ledivdivt 5838  lediv12it 5844  ledivp1t 5853  nn2get 5890  nnleltp1t 5901  lbinfm 5995  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrun 6032  supxrunb1 6036  supxrbnd 6038  zrevaddclt 6117  zltp1let 6128  zextlet 6136  zbtwnre 6169  qrecclt 6211  qrevaddclt 6213  qbtwnre 6216  ser1add2 6275  iooint 6309  elioc2t 6322  elico2t 6323  elicc2t 6324  uz11t 6364  fzaddelt 6432  fzrevt 6443  fzrev3t 6446  fsequb 6455  fsequb2 6456  expcllem 6507  mulexpt 6525  expaddt 6527  divexpt 6530  expmwordit 6537  sqr2irrlem3 6656  seq1bnd 6847  cau2 6850  caubnd 6863  sumeq2 6923  fsum1ps 6956  fsumsplit 6958  fsumcom 6966  fsummulc1 6971  fsumcmpndx2 6980  clm4le 7019  2climnn 7039  2climnn0 7040  climrecl 7047  climaddlem3 7052  climmullem3 7058  climmullem4 7059  climmullem5 7060  climmullem8 7063  climmulc2 7065  climcmpc1 7075  climsqueeze 7076  climsqueeze2 7077  climserzle 7083  climsup 7091  isum1p 7141  isumreclt 7145  cvgratlem2ALT 7183  cvgratlem1 7185  cvgratlem2 7186  cvgratlem5 7189  fsum0diag2 7194  fsum0diag4 7196  elcncf 7200  reeff1o 7368  infxpidmlem1 7495  infxpidmlem11 7505  infxpidmlem12 7506  infxp 7515  infmap2lem2 7522  basgen2t 7581  clsval2 7627  elcls 7646  elcls3 7652  opnssneib 7670  neissex 7679  iscncl 7709  cnconst 7719  dnsconst 7727  mettri3OLD 7759  metxplem4 7773  bl2in 7783  ssblex 7796  metcnplem 7825  metcnp 7826  metcnp2 7827  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnp3 7835  metcnss 7837  bl2ioo 7850  tgioolem 7853  lmconst 7872  lmnn 7873  iscau3 7876  iscauf 7877  causs 7890  lmle 7895  metelcls 7900  metcnp4lem2 7903  metcn4 7905  xplmi 7907  xpcn 7910  bopcnlem2 7916  iscms2lem5 7927  cmsss 7931  cncms 7932  bcthlem9 7941  bcthlem11 7943  bcthlem16 7948  bcthlem19 7951  bcthlem20 7952  bcthlem21 7953  bcthlem24 7956  bcthlem25 7957  bcthlem26 7958  bcthlem29 7961  grpidinvlem3 7984  grplcan 8010  isgrp2i 8011  nvmul0or 8212  nmcnilem 8272  sm1cnilem 8281  sspmval 8326  sspival 8331  sspimsval 8333  nvcnpi4 8355  nmoub3i 8368  0lno 8382  blocnilem 8395  blocni 8396  sspph 8446  ubthlem3 8462  ubthlem5 8464  ubthlem8 8467  ubthlem10 8469  minveclem9 8484  minveclem27 8502  minveclem30 8505  minveclem31 8506  h2hcau 8788  hvmul0ort 8815  hvaddsub4t 8866  hhcms 8993  hhsscms 9067  chocuni 9088  occllem6 9094  projlem25 9126  projlem26 9127  projlem28 9129  shsel3t 9194  shsel1t 9200  spansncol 9407  pjspansnt 9417  5oalem2 9517  5oalem4 9519  3oalem2 9525  eigpos 9679  hhlno 9743  nmopub2tALT 9750  unoplint 9760  nmfnleub2t 9766  hmopadj2t 9781  hmoplint 9782  kbpjt 9796  eighmortht 9804  nmcopexlem6 9871  lnopcon 9878  nmcfnexlem6 9900  lnfncon 9905  nlelch 9909  riesz3 9910  cnlnadjlem6 9920  adjaddt 9940  branmfnt 9951  bra11 9954  leop2t 9969  leopaddt 9977  leopmulit 9978  leoptrit 9981  leopnmidt 9982  nmopleidt 9983  pjss2co 10003  pjssdif1 10014  pj3s 10045  pj3cor1 10047  hstlet 10067  cvcon3t 10121  mdbr2 10133  dmdbr2 10140  mddmd 10144  mdslmd2 10165  csmdsym 10169  superpos 10189  atord 10219  atcvatlem 10220  irredlem1 10225  irred 10229  mdsymlem1 10238  mdsymlem2 10239  mdsymlem3 10240  mdsymlem4 10241  mdsymlem5 10242  sumdmdi 10249  cdj3 10273  mapudiscn 10399  iintlem1 10476
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 147  df-an 225
Copyright terms: Public domain