Theorem adantlr 395

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 391	. 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 411  ad2ant2rl 413  anabss5 504  3ad2antl1 811  3ad2antl2 812  3adant1r 855  ax11eq 1365  ax11el 1366  ax11indalem 1370  ax11inda2ALT 1371  tz7.7 2979  onmindif2 3067  peano5 3159  relop 3281  fvelimab 3771  ssimaex 3774  eqfnfv 3803  fconst2g 3851  isocnv 3902  isotr 3903  isotrALT 3904  tfrlem2 3918  oaordi 4186  oawordri 4190  oaass 4201  omlimcl 4215  odi 4216  omass 4217  oeordi 4220  oewordri 4225  oaabs 4258  omsmolem 4262  omsmo 4263  xpdom2 4448  sbthlem9 4461  mapenlem1 4495  mapenlem2 4496  mapxpen 4501  xpmapenlem3 4504  xpmapenlem4 4505  fiint 4572  fiintOLD 4573  noinfep 4650  aceq5 4750  ac6lem 4764  zorn2lem6 4803  zorn2lem7 4804  fodom 4808  unxpdomlem 4854  axrepndlem2 4957  axrepnd 4958  axpowndlem2 4962  axacndlem5 4975  axacnd 4976  mulcanpi 5039  indpi 5046  genpnmax 5122  addclprlem2 5131  mulclprlem 5133  prlem934b 5150  ssgt0sr 5229  cnegextlem1 5357  cnegextlem3 5359  cnegext 5360  1re 5447  axsup 5519  xrlttrt 5565  divadddivt 5786  divcan6t 5793  ltmul12it 5843  lemul12ait 5844  lemul12itOLD 5845  lemuldivtOLD 5877  ledivdivt 5892  lediv12it 5898  ledivp1t 5907  nn2get 5944  nnleltp1t 5956  lbinfm 6050  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  supxrun 6087  supxrunb1 6091  supxrbnd 6093  zrevaddclt 6172  zltp1let 6183  zextlet 6191  zbtwnre 6223  qrecclt 6274  qrevaddclt 6276  qbtwnre 6279  ser1add2 6339  iooint 6373  elioc2t 6391  elico2t 6392  elicc2t 6393  ioojoint 6417  uz11t 6433  fzaddelt 6501  fzrevt 6512  fzrev3t 6515  fsequb 6524  fsequb2 6525  expcllem 6576  mulexpt 6595  expaddt 6597  divexpt 6600  expmwordit 6607  expnlbndt 6656  sqr2irrlem3 6727  seq1bnd 6910  cau2 6913  caubnd 6926  sumeq2 6985  fsum1ps 7018  fsumsplit 7020  fsumcom 7028  fsummulc1 7033  fsumcmpndx2 7042  clm4le 7081  2climnn 7102  2climnn0 7103  climrecl 7110  climaddlem3 7116  climmullem3 7122  climmullem4 7123  climmullem5 7124  climmullem8 7127  climmulc2 7129  climcmpc1 7139  climsqueeze 7140  climsqueeze2 7141  climserzle 7147  climsup 7155  isum1p 7206  isumreclt 7210  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem2 7251  cvgratlem5 7254  fsum0diag2 7259  fsum0diag4 7261  elcncf 7265  reeff1o 7426  infxpidmlem1 7553  infxpidmlem11 7563  infxpidmlem12 7564  infxp 7573  infmap2lem2 7582  basgen2t 7638  clsval2 7682  elcls 7701  elcls3 7708  opnssneib 7726  neissex 7735  iscnp2 7758  iscncl 7767  cnconst 7777  dnsconst 7785  metxplem4 7830  bl2in 7840  ssblex 7853  metcnplem 7883  metcnp 7884  metcnp2 7885  metcnpi3 7889  metcnpi4 7890  metcni2 7892  metcnp3 7893  metcnss 7895  bl2ioo 7908  tgioolem 7911  lmconst 7931  lmnn 7932  iscau3 7935  iscauf 7936  iscau4 7937  causs 7952  lmle 7957  metelcls 7962  metcnp4lem2 7966  metcn4 7968  xplmi 7970  xpcn 7973  bopcnlem2 7979  iscms2lem5 7990  cmsss 7994  cncms 7995  bcthlem9 8004  bcthlem11 8006  bcthlem16 8011  bcthlem19 8014  bcthlem20 8015  bcthlem21 8016  bcthlem24 8019  bcthlem25 8020  bcthlem26 8021  bcthlem29 8024  grpidinvlem3 8047  grplcan 8071  isgrp2i 8072  nvmul0or 8268  nmcnilem 8333  sm1cnilem 8343  sspmval 8388  sspival 8393  sspimsval 8395  nvcnpi3 8418  nvcnpi4 8419  nmoub3i 8432  0lno 8446  blocnilem 8460  blocni 8461  sspph 8511  ubthlem3 8527  ubthlem5 8529  ubthlem8 8532  ubthlem10 8534  minveclem9 8549  minveclem27 8567  minveclem30 8570  minveclem31 8571  spwpr4OLD 8658  spwpr4aOLD 8659  abssinper 8707  h2hcau 8844  hvmul0ort 8889  hvaddsub4t 8940  hhcms 9067  hhsscms 9145  chocuni 9167  occllem6 9173  projlem25 9205  projlem26 9206  projlem28 9208  shsel3t 9274  shsel1t 9280  spansncol 9486  pjspansnt 9495  5oalem2 9595  5oalem4 9597  3oalem2 9603  eigpos 9757  hhlno 9821  nmopub2tALT 9828  unoplint 9839  nmfnleub2t 9845  hmopadj2t 9860  hmoplint 9861  kbpjt 9875  eighmortht 9883  nmcopexlem6 9951  lnopcon 9958  nmcfnexlem6 9980  lnfncon 9985  nlelch 9989  riesz3 9990  cnlnadjlem6 10000  adjaddt 10021  branmfnt 10033  bra11 10036  leop2t 10052  leopaddt 10060  leopmulit 10061  leoptrit 10064  leopnmidt 10066  nmopleidt 10067  pjss2co 10087  pjssdif1 10098  pj3s 10130  pj3cor1 10132  hstlet 10152  cvcon3t 10206  mdbr2 10218  dmdbr2 10225  mddmd 10231  mdslmd2 10252  csmdsym 10256  superpos 10276  atord 10306  atcvatlem 10307  irredlem1 10312  irred 10316  mdsymlem1 10325  mdsymlem2 10326  mdsymlem3 10327  mdsymlem4 10328  mdsymlem5 10329  sumdmdi 10337  cdj3 10363  mapudiscn 10498  iintlem1 10603

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