Theorem 3ad2antr1 1207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr1  1213  simpr1l  1249  simpr1r  1250  simpr11  1276  simpr12  1277  simpr13  1278  ispod  5572  funcnvqp  6598  dfwe2  7774  poxp  8127  cfcoflem  10277  axdc3lem  10455  fzadd2  13617  fzosubel2  13784  hashdifpr  14483  pfxccat3a  14810  sqrt0  15331  iscatd2  17772  funcestrcsetclem9  18239  funcsetcestrclem9  18254  curf2cl  18322  yonedalem4c  18368  grpsubadd  19154  mulgnnass  19235  mulgnn0ass  19236  dprdss  20161  dprd2da  20174  srgdilem  20334  lsssn0  21135  zntoslem  21772  sraassab  22086  blsscls  24736  iimulcl  25168  pi1grplem  25280  pi1xfrf  25284  dvconst  26147  logexprlim  27464  wwlksnextbi  30365  clwwlkccatlem  30462  clwwlkccat  30463  umgr3cyclex  30666  nvss  31077  disjdsct  33178  idlsrgmnd  33927  issgon  34636  measdivcst  34738  measdivcstALTV  34739  prv1n  36013  elmrsubrn  36102  poimirlem28  38400  ftc1anc  38453  fdc  38498  cvrnbtwn3  40152  paddasslem9  40704  paddasslem17  40712  pmapjlln1  40731  lautj  40969  lautm  40970  dfsalgen2  47172  smflimlem4  47605  lidldomnnring  49154  funcringcsetcALTV2lem9  49216  funcringcsetclem9ALTV  49239  lincresunit3lem2  49413  isthincd2  50366