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 1362  ax11el 1363  ax11indalem 1367  ax11inda2ALT 1368  tz7.7 2969  onmindif2 3057  peano5 3149  relop 3271  fvelimab 3760  ssimaex 3763  eqfnfv 3792  fconst2g 3840  isocnv 3891  isotr 3892  isotrALT 3893  tfrlem2 3907  oaordi 4173  oawordri 4177  oaass 4188  omlimcl 4202  odi 4203  omass 4204  oeordi 4207  oewordri 4212  oaabs 4245  omsmolem 4249  omsmo 4250  xpdom2 4431  sbthlem9 4444  mapenlem1 4478  mapenlem2 4479  mapxpen 4484  xpmapenlem3 4487  xpmapenlem4 4488  fiint 4543  fodomfib 4550  noinfep 4623  aceq5 4723  ac6lem 4737  zorn2lem6 4776  zorn2lem7 4777  fodom 4781  unxpdomlem 4826  axrepndlem2 4928  axrepnd 4929  axpowndlem2 4933  axacndlem5 4946  axacnd 4947  mulcanpi 5010  indpi 5017  genpnmax 5093  addclprlem2 5102  mulclprlem 5104  prlem934b 5121  ssgt0sr 5200  cnegextlem1 5328  cnegextlem3 5330  cnegext 5331  1re 5418  axsup 5490  xrlttrt 5536  divadddivt 5750  divcan6t 5757  ltmul12it 5807  lemul12ait 5808  lemul12itOLD 5809  lemuldivt 5834  ledivdivt 5848  lediv12it 5854  ledivp1t 5863  nn2get 5900  nnleltp1t 5911  lbinfm 6005  xrsupsslem 6033  xrinfmsslem 6034  xrub 6037  supxrun 6042  supxrunb1 6046  supxrbnd 6048  zrevaddclt 6127  zltp1let 6138  zextlet 6146  zbtwnre 6179  qrecclt 6223  qrevaddclt 6225  qbtwnre 6228  ser1add2 6288  iooint 6322  elioc2t 6335  elico2t 6336  elicc2t 6337  uz11t 6377  fzaddelt 6445  fzrevt 6456  fzrev3t 6459  fsequb 6468  fsequb2 6469  expcllem 6520  mulexpt 6539  expaddt 6541  divexpt 6544  expmwordit 6551  expnlbndt 6600  sqr2irrlem3 6671  seq1bnd 6862  cau2 6865  caubnd 6878  sumeq2 6938  fsum1ps 6971  fsumsplit 6973  fsumcom 6981  fsummulc1 6986  fsumcmpndx2 6995  clm4le 7034  2climnn 7055  2climnn0 7056  climrecl 7063  climaddlem3 7069  climmullem3 7075  climmullem4 7076  climmullem5 7077  climmullem8 7080  climmulc2 7082  climcmpc1 7092  climsqueeze 7093  climsqueeze2 7094  climserzle 7100  climsup 7108  isum1p 7158  isumreclt 7162  cvgratlem2ALT 7200  cvgratlem1 7202  cvgratlem2 7203  cvgratlem5 7206  fsum0diag2 7211  fsum0diag4 7213  elcncf 7217  reeff1o 7385  infxpidmlem1 7512  infxpidmlem11 7522  infxpidmlem12 7523  infxp 7532  infmap2lem2 7540  basgen2t 7599  clsval2 7645  elcls 7664  elcls3 7671  opnssneib 7689  neissex 7698  iscnp2 7721  iscncl 7730  cnconst 7740  dnsconst 7748  mettri3OLD 7780  metxplem4 7795  bl2in 7805  ssblex 7818  metcnplem 7848  metcnp 7849  metcnp2 7850  metcnpi3 7854  metcnpi4 7855  metcni2 7857  metcnp3 7858  metcnss 7860  bl2ioo 7873  tgioolem 7876  lmconst 7896  lmnn 7897  iscau3 7900  iscauf 7901  iscau4 7902  causs 7917  lmle 7922  metelcls 7927  metcnp4lem2 7931  metcn4 7933  xplmi 7935  xpcn 7938  bopcnlem2 7944  iscms2lem5 7955  cmsss 7959  cncms 7960  bcthlem9 7969  bcthlem11 7971  bcthlem16 7976  bcthlem19 7979  bcthlem20 7980  bcthlem21 7981  bcthlem24 7984  bcthlem25 7985  bcthlem26 7986  bcthlem29 7989  grpidinvlem3 8012  grplcan 8037  isgrp2i 8038  nvmul0or 8236  nmcnilem 8300  sm1cnilem 8309  sspmval 8354  sspival 8359  sspimsval 8361  nvcnpi4 8383  nmoub3i 8396  0lno 8410  blocnilem 8423  blocni 8424  sspph 8474  ubthlem3 8490  ubthlem5 8492  ubthlem8 8495  ubthlem10 8497  minveclem9 8512  minveclem27 8530  minveclem30 8533  minveclem31 8534  h2hcau 8804  hvmul0ort 8849  hvaddsub4t 8900  hhcms 9027  hhsscms 9105  chocuni 9127  occllem6 9133  projlem25 9165  projlem26 9166  projlem28 9168  shsel3t 9234  shsel1t 9240  spansncol 9447  pjspansnt 9457  5oalem2 9557  5oalem4 9559  3oalem2 9565  eigpos 9719  hhlno 9783  nmopub2tALT 9790  unoplint 9801  nmfnleub2t 9807  hmopadj2t 9822  hmoplint 9823  kbpjt 9837  eighmortht 9845  nmcopexlem6 9912  lnopcon 9919  nmcfnexlem6 9941  lnfncon 9946  nlelch 9950  riesz3 9951  cnlnadjlem6 9961  adjaddt 9982  branmfnt 9994  bra11 9997  leop2t 10013  leopaddt 10021  leopmulit 10022  leoptrit 10025  leopnmidt 10027  nmopleidt 10028  pjss2co 10048  pjssdif1 10059  pj3s 10091  pj3cor1 10093  hstlet 10113  cvcon3t 10167  mdbr2 10179  dmdbr2 10186  mddmd 10192  mdslmd2 10213  csmdsym 10217  superpos 10237  atord 10267  atcvatlem 10268  irredlem1 10273  irred 10277  mdsymlem1 10286  mdsymlem2 10287  mdsymlem3 10288  mdsymlem4 10289  mdsymlem5 10290  sumdmdi 10298  cdj3 10324  mapudiscn 10458  iintlem1 10548

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