Theorem 3ad2antr1 1189

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpr1  1195  simpr1l  1231  simpr1r  1232  simpr11  1258  simpr12  1259  simpr13  1260  ispod  5531  funcnvqp  6545  dfwe2  7707  poxp  8058  cfcoflem  10163  axdc3lem  10341  fzadd2  13459  fzosubel2  13625  hashdifpr  14322  pfxccat3a  14645  sqrt0  15148  iscatd2  17587  funcestrcsetclem9  18054  funcsetcestrclem9  18069  curf2cl  18137  yonedalem4c  18183  grpsubadd  18941  mulgnnass  19022  mulgnn0ass  19023  dprdss  19943  dprd2da  19956  srgdilem  20110  lsssn0  20881  zntoslem  21493  sraassab  21805  blsscls  24422  iimulcl  24860  pi1grplem  24976  pi1xfrf  24980  dvconst  25845  logexprlim  27163  wwlksnextbi  29872  clwwlkccatlem  29969  clwwlkccat  29970  umgr3cyclex  30163  nvss  30573  disjdsct  32684  idlsrgmnd  33479  issgon  34136  measdivcst  34237  measdivcstALTV  34238  prv1n  35475  elmrsubrn  35564  poimirlem28  37698  ftc1anc  37751  fdc  37795  cvrnbtwn3  39385  paddasslem9  39937  paddasslem17  39945  pmapjlln1  39964  lautj  40202  lautm  40203  dfsalgen2  46449  smflimlem4  46882  lidldomnnring  48346  funcringcsetcALTV2lem9  48408  funcringcsetclem9ALTV  48431  lincresunit3lem2  48591  isthincd2  49548