Theorem 3ad2antr1 1186

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

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

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 1087

This theorem is referenced by:  simpr1  1192  simpr1l  1228  simpr1r  1229  simpr11  1255  simpr12  1256  simpr13  1257  ispod  5596  funcnvqp  6611  dfwe2  7763  poxp  8116  cfcoflem  10269  axdc3lem  10447  fzadd2  13540  fzosubel2  13696  hashdifpr  14379  pfxccat3a  14692  sqrt0  15192  iscatd2  17629  funcestrcsetclem9  18104  funcsetcestrclem9  18119  curf2cl  18188  yonedalem4c  18234  grpsubadd  18947  mulgnnass  19025  mulgnn0ass  19026  dprdss  19940  dprd2da  19953  srgdilem  20086  lsssn0  20702  zntoslem  21331  sraassab  21641  psrbaglesuppOLD  21697  blsscls  24236  iimulcl  24680  pi1grplem  24796  pi1xfrf  24800  dvconst  25666  logexprlim  26964  wwlksnextbi  29415  clwwlkccatlem  29509  clwwlkccat  29510  umgr3cyclex  29703  nvss  30113  disjdsct  32191  idlsrgmnd  32902  issgon  33419  measdivcst  33520  measdivcstALTV  33521  prv1n  34720  elmrsubrn  34809  poimirlem28  36819  ftc1anc  36872  fdc  36916  cvrnbtwn3  38449  paddasslem9  39002  paddasslem17  39010  pmapjlln1  39029  lautj  39267  lautm  39268  dfsalgen2  45355  smflimlem4  45788  lidldomnnring  46916  funcringcsetcALTV2lem9  47030  funcringcsetclem9ALTV  47053  lincresunit3lem2  47248  isthincd2  47745