Theorem adantrr 404

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
adantrr	|- ((ph /\ (ps /\ th)) -> ch)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 380	. . 3 |- (ph -> (ps -> ch))
3	2	adantrd 400	. 2 |- (ph -> ((ps /\ th) -> ch))
4	3	imp 357	1 |- ((ph /\ (ps /\ th)) -> ch)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  ad2ant2r 418  ad2ant2lr 419  anabss1 510  3ad2antr1 824  sbcom 1300  ax11eq 1405  ax11el 1406  ifboth 2427  po2nr 2903  sotric 2916  tz7.7 3030  ordsucun 3139  opelxp1 3262  isocnv 3954  isomin 3957  isoini 3958  oalim 4225  omlim 4226  oaass 4253  omordi 4255  omwordri 4261  odi 4268  oen0 4271  oewordri 4277  oeworde 4278  dom2d 4465  ssenen 4569  ssfi 4601  inf3lem6 4680  rankxplim3 4776  aceq5lem4 4800  aceq6b 4804  unidom 4870  axacndlem4 5027  ltapq 5141  ltmpq 5142  ltexpq 5145  ltexprlem6 5212  ssgt0sr 5282  add4 5403  2addsub 5454  mul4 5485  muladd 5486  xrlttr 5618  ltleadd 5710  divmul3 5776  rec11r 5837  divdivdiv 5843  divdiv23 5850  lemul2a 5897  lemul12b 5900  ltmuldiv2 5923  ltdivmul 5925  ledivmul 5927  ltdivmul2 5929  ledivmul2 5932  lemuldiv2 5936  ltdiv23 5952  lediv23 5953  suprleub 6141  infmrcl 6151  xrsupsslem 6158  xrinfmsslem 6159  supxrunb1 6171  supxrunb2 6172  supxrleub 6181  zextlt 6275  zmax 6305  qbtwnre 6331  modadd1 6380  iooshf 6421  icounlem 6438  ioojoin 6442  recexp 6684  expsub 6687  expordi 6689  expord2 6693  sqlecan 6730  lenegsq 6975  seq1ublem 7001  fsumcom 7118  fsumshf 7121  2climnni 7192  2climnn0i 7193  climge0 7202  climaddlem3 7206  climmullem1 7210  climmullem3 7212  climmullem5 7214  climmullem8 7217  climsqueeze 7230  climsqueeze2 7231  climcaui 7246  serzf0i 7259  ser1f0i 7260  ser1cmp2i 7267  cvgratlem2 7341  cvgratlem5 7344  fsum0diaglem2 7347  mulc1cncf 7369  acdc3lem 7578  acdclem 7586  infxpidmlem7 7650  infxpidmlem12 7655  eltg2 7708  tgcl 7713  tgval3 7714  tgss2 7726  2basgen 7730  iscld 7754  ntrss 7773  ssnei2 7815  neindisj 7816  islp2 7832  cnpcl 7849  dnsconst 7873  ismsg 7885  blss 7938  blssex 7939  metcnp 7972  metcnpi3 7977  metcnpi4 7978  metcni2 7980  tgioolem 7999  lmss 8038  lmle 8045  metelcls 8050  metcnp4 8055  xplmi 8058  xpcn 8061  lmcau 8081  cmsss 8082  bcthlem11 8094  bcthlem15 8098  bcthlem18 8101  bcthlem19 8102  bcthlem20 8103  bcthlem21 8104  bcthlem24 8107  grpidinv 8137  grprcan 8147  grpinvid1 8156  grpinvid2 8157  grplcan 8159  abl4 8189  isring 8225  nvsubadd 8359  nvabs 8385  va1cnlem 8429  nvcnpi3 8506  nvcnpi4 8507  sspph 8599  ubthlem3 8615  ubthlem9 8621  ubthlem11 8623  ubthlem12 8624  ubthlem14 8626  hvadd4 8988  hvaddsub4 9028  chocunii 9255  occllem6 9261  shscli 9364  pjspansn 9583  fh1 9644  fh2 9645  cm2j 9646  spansncvi 9680  5oalem2 9683  5oalem5 9686  5oalem6 9687  3oalem2 9691  hoadd4 9793  cnvunop 9925  bralnfn 9955  eighmorth 9971  hmops 10028  hmopm 10029  hmopco 10031  lnopconi 10046  lnfnconi 10073  adjlnop 10102  adjmul 10108  adjadd 10109  nmopcoi 10111  kbass6 10137  hstle 10241  stlesi 10252  strlem3a 10263  hstrlem3a 10271  mdsl0 10321  mdexchi 10346  atom1d 10364  superpos 10365  cvexchlem 10379  atomli 10393  atcvatlem 10396  irredlem2 10402  irredlem3 10403  atcvat4i 10408  mdsymlem1 10414  mdsymlem3 10416  mdsymlem5 10418  mdsymlem6 10419  sumdmdlem 10429  sumdmdlem2 10430  cdj1i 10444  cdj3lem2b 10448  nndivsub 10508  iepiclem 10833

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