Theorem 3ad2antr1 1185

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 1168	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simpr1  1191  simpr1l  1227  simpr1r  1228  simpr11  1254  simpr12  1255  simpr13  1256  ispod  5603  funcnvqp  6623  dfwe2  7782  poxp  8142  cfcoflem  10315  axdc3lem  10493  fzadd2  13590  fzosubel2  13746  hashdifpr  14432  pfxccat3a  14746  sqrt0  15246  iscatd2  17694  funcestrcsetclem9  18172  funcsetcestrclem9  18187  curf2cl  18256  yonedalem4c  18302  grpsubadd  19022  mulgnnass  19103  mulgnn0ass  19104  dprdss  20029  dprd2da  20042  srgdilem  20175  lsssn0  20925  zntoslem  21554  sraassab  21865  psrbaglesuppOLD  21922  blsscls  24507  iimulcl  24951  pi1grplem  25067  pi1xfrf  25071  dvconst  25937  logexprlim  27254  wwlksnextbi  29828  clwwlkccatlem  29922  clwwlkccat  29923  umgr3cyclex  30116  nvss  30526  disjdsct  32614  idlsrgmnd  33389  issgon  33956  measdivcst  34057  measdivcstALTV  34058  prv1n  35259  elmrsubrn  35348  poimirlem28  37349  ftc1anc  37402  fdc  37446  cvrnbtwn3  38974  paddasslem9  39527  paddasslem17  39535  pmapjlln1  39554  lautj  39792  lautm  39793  dfsalgen2  45962  smflimlem4  46395  lidldomnnring  47613  funcringcsetcALTV2lem9  47675  funcringcsetclem9ALTV  47698  lincresunit3lem2  47863  isthincd2  48359