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 373	. . 3 |- (ph -> (ps -> ch))
3	2	adantr 389	. 2 |- ((ph /\ th) -> (ps -> ch))
4	3	imp 350	1 |- (((ph /\ th) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ad2ant2r 409  ad2ant2rl 411  anabss5 502  3ad2antl1 808  3ad2antl2 809  3adant1r 852  ax11eq 1361  ax11el 1362  ax11indalem 1366  ax11inda2ALT 1367  tz7.7 2968  onmindif2 3056  peano5 3148  relop 3270  fvelimab 3756  ssimaex 3759  eqfnfv 3788  fconst2g 3836  isocnv 3887  isotr 3888  isotrALT 3889  tfrlem2 3903  oaordi 4170  oawordri 4174  oaass 4185  omlimcl 4199  odi 4200  omass 4201  oeordi 4204  oewordri 4209  oaabs 4242  omsmolem 4246  omsmo 4247  xpdom2 4428  sbthlem9 4441  mapenlem1 4475  mapenlem2 4476  mapxpen 4481  xpmapenlem3 4484  xpmapenlem4 4485  fiint 4540  fodomfib 4547  noinfep 4620  aceq5 4720  ac6lem 4734  zorn2lem6 4773  zorn2lem7 4774  fodom 4778  unxpdomlem 4823  axrepndlem2 4925  axrepnd 4926  axpowndlem2 4930  axacndlem5 4943  axacnd 4944  mulcanpi 5007  indpi 5014  genpnmax 5090  addclprlem2 5099  mulclprlem 5101  prlem934b 5118  ssgt0sr 5197  cnegextlem1 5325  cnegextlem3 5327  cnegext 5328  1re 5415  axsup 5487  xrlttrt 5534  divadddivt 5748  divcan6t 5755  ltmul12it 5805  lemul12ait 5806  lemul12itOLD 5807  lemuldivt 5832  ledivdivt 5846  lediv12it 5852  ledivp1t 5861  nn2get 5898  nnleltp1t 5909  lbinfm 6003  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxrun 6040  supxrunb1 6044  supxrbnd 6046  zrevaddclt 6125  zltp1let 6136  zextlet 6144  zbtwnre 6177  qrecclt 6219  qrevaddclt 6221  qbtwnre 6224  ser1add2 6283  iooint 6317  elioc2t 6330  elico2t 6331  elicc2t 6332  uz11t 6372  fzaddelt 6440  fzrevt 6451  fzrev3t 6454  fsequb 6463  fsequb2 6464  expcllem 6515  mulexpt 6533  expaddt 6535  divexpt 6538  expmwordit 6545  sqr2irrlem3 6664  seq1bnd 6855  cau2 6858  caubnd 6871  sumeq2 6931  fsum1ps 6964  fsumsplit 6966  fsumcom 6974  fsummulc1 6979  fsumcmpndx2 6988  clm4le 7027  2climnn 7047  2climnn0 7048  climrecl 7055  climaddlem3 7060  climmullem3 7066  climmullem4 7067  climmullem5 7068  climmullem8 7071  climmulc2 7073  climcmpc1 7083  climsqueeze 7084  climsqueeze2 7085  climserzle 7091  climsup 7099  isum1p 7149  isumreclt 7153  cvgratlem2ALT 7191  cvgratlem1 7193  cvgratlem2 7194  cvgratlem5 7197  fsum0diag2 7202  fsum0diag4 7204  elcncf 7208  reeff1o 7376  infxpidmlem1 7503  infxpidmlem11 7513  infxpidmlem12 7514  infxp 7523  infmap2lem2 7530  basgen2t 7589  clsval2 7635  elcls 7654  elcls3 7661  opnssneib 7679  neissex 7688  iscnp2 7711  iscncl 7720  cnconst 7730  dnsconst 7738  mettri3OLD 7770  metxplem4 7785  bl2in 7795  ssblex 7808  metcnplem 7838  metcnp 7839  metcnp2 7840  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metcnp3 7848  metcnss 7850  bl2ioo 7863  tgioolem 7866  lmconst 7886  lmnn 7887  iscau3 7890  iscauf 7891  iscau4 7892  causs 7906  lmle 7911  metelcls 7916  metcnp4lem2 7919  metcn4 7921  xplmi 7923  xpcn 7926  bopcnlem2 7932  iscms2lem5 7943  cmsss 7947  cncms 7948  bcthlem9 7957  bcthlem11 7959  bcthlem16 7964  bcthlem19 7967  bcthlem20 7968  bcthlem21 7969  bcthlem24 7972  bcthlem25 7973  bcthlem26 7974  bcthlem29 7977  grpidinvlem3 8000  grplcan 8025  isgrp2i 8026  nvmul0or 8224  nmcnilem 8285  sm1cnilem 8294  sspmval 8339  sspival 8344  sspimsval 8346  nvcnpi4 8368  nmoub3i 8381  0lno 8395  blocnilem 8408  blocni 8409  sspph 8459  ubthlem3 8475  ubthlem5 8477  ubthlem8 8480  ubthlem10 8482  minveclem9 8497  minveclem27 8515  minveclem30 8518  minveclem31 8519  h2hcau 8788  hvmul0ort 8833  hvaddsub4t 8884  hhcms 9011  hhsscms 9089  chocuni 9111  occllem6 9117  projlem25 9149  projlem26 9150  projlem28 9152  shsel3t 9217  shsel1t 9223  spansncol 9430  pjspansnt 9440  5oalem2 9540  5oalem4 9542  3oalem2 9548  eigpos 9702  hhlno 9766  nmopub2tALT 9773  unoplint 9783  nmfnleub2t 9789  hmopadj2t 9804  hmoplint 9805  kbpjt 9819  eighmortht 9827  nmcopexlem6 9894  lnopcon 9901  nmcfnexlem6 9923  lnfncon 9928  nlelch 9932  riesz3 9933  cnlnadjlem6 9943  adjaddt 9964  branmfnt 9976  bra11 9979  leop2t 9995  leopaddt 10003  leopmulit 10004  leoptrit 10007  leopnmidt 10009  nmopleidt 10010  pjss2co 10030  pjssdif1 10041  pj3s 10073  pj3cor1 10075  hstlet 10095  cvcon3t 10149  mdbr2 10161  dmdbr2 10168  mddmd 10173  mdslmd2 10194  csmdsym 10198  superpos 10218  atord 10248  atcvatlem 10249  irredlem1 10254  irred 10258  mdsymlem1 10267  mdsymlem2 10268  mdsymlem3 10269  mdsymlem4 10270  mdsymlem5 10271  sumdmdi 10278  cdj3 10302  mapudiscn 10435  iintlem1 10512

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