Theorem 3ad2antr1 1203

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 400  df-3an 1101

This theorem is referenced by:  simpr1  1209  simpr1l  1245  simpr1r  1246  simpr11  1272  simpr12  1273  simpr13  1274  ispod  5565  funcnvqp  6586  dfwe2  7758  poxp  8109  cfcoflem  10230  axdc3lem  10408  fzadd2  13565  fzosubel2  13732  hashdifpr  14429  pfxccat3a  14752  sqrt0  15269  iscatd2  17714  funcestrcsetclem9  18181  funcsetcestrclem9  18196  curf2cl  18264  yonedalem4c  18310  grpsubadd  19071  mulgnnass  19152  mulgnn0ass  19153  dprdss  20072  dprd2da  20085  srgdilem  20243  lsssn0  21016  zntoslem  21609  sraassab  21921  blsscls  24568  iimulcl  25000  pi1grplem  25112  pi1xfrf  25116  dvconst  25980  logexprlim  27290  wwlksnextbi  30095  clwwlkccatlem  30192  clwwlkccat  30193  umgr3cyclex  30386  nvss  30797  disjdsct  32906  idlsrgmnd  33711  issgon  34421  measdivcst  34522  measdivcstALTV  34523  prv1n  35782  elmrsubrn  35871  poimirlem28  38148  ftc1anc  38201  fdc  38245  cvrnbtwn3  39901  paddasslem9  40453  paddasslem17  40461  pmapjlln1  40480  lautj  40718  lautm  40719  dfsalgen2  46916  smflimlem4  47349  lidldomnnring  48859  funcringcsetcALTV2lem9  48921  funcringcsetclem9ALTV  48944  lincresunit3lem2  49103  isthincd2  50059