Theorem adantrr 395

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ad2ant2r 409  ad2ant2lr 410  anabss1 499  3ad2antr1 811  sbcom 1256  ax11eq 1361  ax11el 1362  ifboth 2371  po2nr 2842  sotric 2855  tz7.7 2968  ordsucun 3077  opelxp1 3200  isocnv 3887  isomin 3890  isoini 3891  oalim 4157  omlim 4158  oaass 4185  omordi 4187  omwordri 4193  odi 4200  oen0 4203  oewordri 4209  oeworde 4210  dom2d 4391  ssenen 4490  ssfi 4521  inf3lem6 4598  rankxplim3 4694  aceq5lem4 4718  aceq6b 4722  unidom 4788  axacndlem4 4942  ltapq 5056  ltmpq 5057  ltexpq 5060  ltexprlem6 5127  ssgt0sr 5197  add4t 5318  2addsubt 5369  mul4t 5400  muladdt 5401  xrlttrt 5534  ltleaddt 5627  rec11rt 5743  divdivdivt 5749  divdiv23t 5756  lemul2it 5803  lemul12ait 5806  ltdiv23t 5848  lediv23t 5849  suprleub 6014  infmrcl 6024  xrsupsslem 6031  xrinfmsslem 6032  supxrunb1 6044  supxrunb2 6045  supxrleub 6054  zextltt 6145  zmax 6176  qbtwnre 6224  icounlem 6353  recexpt 6534  expsubt 6537  expordit 6539  expord2t 6543  sqlecant 6580  lenegsqt 6831  seq1ublem 6856  fsumcom 6974  fsumshft 6977  2climnn 7047  2climnn0 7048  climge0 7057  climaddlem3 7060  climmullem1 7064  climmullem3 7066  climmullem5 7068  climmullem8 7071  climsqueeze 7084  climsqueeze2 7085  climcau 7100  serzf0 7113  ser1f0 7114  ser1cmp2 7121  cvgratlem2 7194  cvgratlem5 7197  fsum0diaglem2 7200  mulc1cncf 7222  acdc3lem 7436  acdclem 7444  infxpidmlem7 7509  infxpidmlem12 7514  eltg2t 7569  tgclt 7574  tgval3t 7575  tgss2t 7587  2basgent 7591  iscld 7619  ntrss 7638  ssnei2 7680  neindisj 7681  islp2 7697  cnpcl 7714  dnsconst 7738  ismsg 7750  blss 7805  blssex 7806  metcnp 7839  metcnpi3 7844  metcnpi4 7845  metcni2 7847  tgioolem 7866  lmss 7904  lmle 7911  metelcls 7916  metcnp4 7920  xplmi 7923  xpcn 7926  lmcau 7946  cmsss 7947  bcthlem11 7959  bcthlem15 7963  bcthlem18 7966  bcthlem19 7967  bcthlem20 7968  bcthlem21 7969  bcthlem24 7972  grpidinv 8002  grprcan 8013  grpinvid1 8022  grpinvid2 8023  grplcan 8025  abl4 8056  isring 8093  nvsubadd 8227  nvabs 8253  va1cnlem 8292  nvcnpi4 8368  sspph 8459  ubthlem3 8475  ubthlem9 8481  ubthlem11 8483  ubthlem12 8484  ubthlem14 8486  hvadd4t 8844  hvaddsub4t 8884  chocuni 9111  occllem6 9117  shscl 9219  pjspansnt 9440  fh1t 9501  fh2t 9502  cm2jt 9503  spansncv 9537  5oalem2 9540  5oalem5 9543  5oalem6 9544  3oalem2 9548  hoadd4t 9650  cnvunopt 9781  bralnfnt 9811  eighmortht 9827  hmopst 9883  hmopmt 9884  hmopcot 9886  lnopcon 9901  lnfncon 9928  adjlnopt 9957  adjmult 9963  adjaddt 9964  nmopco 9966  kbass6t 9992  hstlet 10095  stles 10106  strlem3a 10117  hstrlem3a 10125  mdsl0 10174  mdexch 10199  atom1d 10217  superpos 10218  cvexchlem 10232  atoml 10246  atcvatlem 10249  irredlem2 10255  irredlem3 10256  atcvat4 10261  mdsymlem1 10267  mdsymlem3 10269  mdsymlem5 10271  mdsymlem6 10272  sumdmdlem 10281  sumdmdlem2 10282  cdj1 10294  cdj3lem2b 10298  nndivsub 10357

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