Theorem 3ad2antr1 1232

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 699	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
3	2	3adantr3 1205	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simpr1  1241  simpr1l  1298  simpr1r  1300  simpr11  1340  simpr12  1342  simpr13  1344  ispod  5240  funcnvqp  6164  dfwe2  7211  poxp  7523  cfcoflem  9379  axdc3lem  9557  fzadd2  12599  fzosubel2  12752  hashdifpr  13420  sqr0lem  14204  iscatd2  16546  funcestrcsetclem9  16993  funcsetcestrclem9  17008  curf2cl  17076  yonedalem4c  17122  grpsubadd  17708  mulgnnass  17779  mulgnn0ass  17780  dprdss  18630  dprd2da  18643  srgi  18713  lsssn0  19152  psrbaglesupp  19577  zntoslem  20112  blsscls  22525  iimulcl  22949  pi1grplem  23061  pi1xfrf  23065  dvconst  23894  logexprlim  25164  wwlksnextbi  27031  umgr3cyclex  27356  nvss  27776  disjdsct  29807  issgon  30511  measdivcstOLD  30612  measdivcst  30613  elmrsubrn  31740  poimirlem28  33750  ftc1anc  33805  fdc  33852  cvrnbtwn3  35056  paddasslem9  35608  paddasslem17  35616  pmapjlln1  35635  lautj  35873  lautm  35874  dfsalgen2  41038  smflimlem4  41464  pfxccat3a  42004  splvalpfx  42010  lidldomnnring  42498  funcringcsetcALTV2lem9  42612  funcringcsetclem9ALTV  42635  lincresunit3lem2  42837