Theorem 3ad2antr1 1184

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr1  1190  simpr1l  1226  simpr1r  1227  simpr11  1253  simpr12  1254  simpr13  1255  ispod  5484  funcnvqp  6420  dfwe2  7498  poxp  7824  cfcoflem  9696  axdc3lem  9874  fzadd2  12945  fzosubel2  13100  hashdifpr  13779  pfxccat3a  14102  sqr0lem  14602  iscatd2  16954  funcestrcsetclem9  17400  funcsetcestrclem9  17415  curf2cl  17483  yonedalem4c  17529  grpsubadd  18189  mulgnnass  18264  mulgnn0ass  18265  dprdss  19153  dprd2da  19166  srgi  19263  lsssn0  19721  psrbaglesupp  20150  zntoslem  20705  blsscls  23119  iimulcl  23543  pi1grplem  23655  pi1xfrf  23659  dvconst  24516  logexprlim  25803  wwlksnextbi  27674  clwwlkccatlem  27769  clwwlkccat  27770  umgr3cyclex  27964  nvss  28372  disjdsct  30440  issgon  31384  measdivcst  31485  measdivcstALTV  31486  prv1n  32680  elmrsubrn  32769  poimirlem28  34922  ftc1anc  34977  fdc  35022  cvrnbtwn3  36414  paddasslem9  36966  paddasslem17  36974  pmapjlln1  36993  lautj  37231  lautm  37232  dfsalgen2  42631  smflimlem4  43057  lidldomnnring  44208  funcringcsetcALTV2lem9  44322  funcringcsetclem9ALTV  44345  lincresunit3lem2  44542