Theorem 3ad2antr1 1204

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr1	⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3ad2antr1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrr 755	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
3	2	3adantr3 1177	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074

This theorem is referenced by:  simpr1  1234  simpr1l  1291  simpr1r  1293  simpr11  1333  simpr12  1335  simpr13  1337  ispod  5195  funcnvqp  6113  dfwe2  7146  poxp  7457  cfcoflem  9286  axdc3lem  9464  fzadd2  12569  fzosubel2  12722  hashdifpr  13395  sqr0lem  14180  iscatd2  16543  funcestrcsetclem9  16989  funcsetcestrclem9  17004  curf2cl  17072  yonedalem4c  17118  grpsubadd  17704  mulgnnass  17777  mulgnnassOLD  17778  mulgnn0ass  17779  dprdss  18628  dprd2da  18641  srgi  18711  lsssn0  19150  psrbaglesupp  19570  zntoslem  20107  blsscls  22513  iimulcl  22937  pi1grplem  23049  pi1xfrf  23053  dvconst  23879  logexprlim  25149  wwlksnextbi  27012  umgr3cyclex  27335  nvss  27757  disjdsct  29789  issgon  30495  measdivcstOLD  30596  measdivcst  30597  elmrsubrn  31724  poimirlem28  33750  ftc1anc  33806  fdc  33854  cvrnbtwn3  35066  paddasslem9  35617  paddasslem17  35625  pmapjlln1  35644  lautj  35882  lautm  35883  dfsalgen2  41062  smflimlem4  41488  pfxccat3a  41939  splvalpfx  41945  lidldomnnring  42440  funcringcsetcALTV2lem9  42554  funcringcsetclem9ALTV  42577  lincresunit3lem2  42779