Theorem 3ad2antr1 1202

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

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

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 1100

This theorem is referenced by:  simpr1  1208  simpr1l  1244  simpr1r  1245  simpr11  1271  simpr12  1272  simpr13  1273  ispod  5564  funcnvqp  6585  dfwe2  7757  poxp  8108  cfcoflem  10229  axdc3lem  10407  fzadd2  13564  fzosubel2  13731  hashdifpr  14428  pfxccat3a  14751  sqrt0  15268  iscatd2  17713  funcestrcsetclem9  18180  funcsetcestrclem9  18195  curf2cl  18263  yonedalem4c  18309  grpsubadd  19070  mulgnnass  19151  mulgnn0ass  19152  dprdss  20071  dprd2da  20084  srgdilem  20242  lsssn0  21015  zntoslem  21608  sraassab  21920  blsscls  24567  iimulcl  24999  pi1grplem  25111  pi1xfrf  25115  dvconst  25979  logexprlim  27289  wwlksnextbi  30094  clwwlkccatlem  30191  clwwlkccat  30192  umgr3cyclex  30385  nvss  30796  disjdsct  32905  idlsrgmnd  33710  issgon  34420  measdivcst  34521  measdivcstALTV  34522  prv1n  35781  elmrsubrn  35870  poimirlem28  38147  ftc1anc  38200  fdc  38244  cvrnbtwn3  39900  paddasslem9  40452  paddasslem17  40460  pmapjlln1  40479  lautj  40717  lautm  40718  dfsalgen2  46915  smflimlem4  47348  lidldomnnring  48858  funcringcsetcALTV2lem9  48920  funcringcsetclem9ALTV  48943  lincresunit3lem2  49102  isthincd2  50058