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  5580  funcnvqp  6604  dfwe2  7779  poxp  8130  cfcoflem  10271  axdc3lem  10449  fzadd2  13606  fzosubel2  13773  hashdifpr  14472  pfxccat3a  14799  sqrt0  15318  iscatd2  17761  funcestrcsetclem9  18228  funcsetcestrclem9  18243  curf2cl  18311  yonedalem4c  18357  grpsubadd  19140  mulgnnass  19221  mulgnn0ass  19222  dprdss  20147  dprd2da  20160  srgdilem  20320  lsssn0  21121  zntoslem  21758  sraassab  22070  blsscls  24717  iimulcl  25149  pi1grplem  25261  pi1xfrf  25265  dvconst  26129  logexprlim  27442  wwlksnextbi  30312  clwwlkccatlem  30409  clwwlkccat  30410  umgr3cyclex  30607  nvss  31018  disjdsct  33121  idlsrgmnd  33870  issgon  34579  measdivcst  34681  measdivcstALTV  34682  prv1n  35962  elmrsubrn  36051  poimirlem28  38358  ftc1anc  38411  fdc  38456  cvrnbtwn3  40110  paddasslem9  40662  paddasslem17  40670  pmapjlln1  40689  lautj  40927  lautm  40928  dfsalgen2  47115  smflimlem4  47548  lidldomnnring  49060  funcringcsetcALTV2lem9  49122  funcringcsetclem9ALTV  49145  lincresunit3lem2  49319  isthincd2  50274