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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simpr1  1213  simpr1l  1249  simpr1r  1250  simpr11  1276  simpr12  1277  simpr13  1278  ispod  5578  funcnvqp  6600  dfwe2  7769  poxp  8120  cfcoflem  10251  axdc3lem  10429  fzadd2  13583  fzosubel2  13750  hashdifpr  14448  pfxccat3a  14771  sqrt0  15288  iscatd2  17732  funcestrcsetclem9  18199  funcsetcestrclem9  18214  curf2cl  18282  yonedalem4c  18328  grpsubadd  19089  mulgnnass  19170  mulgnn0ass  19171  dprdss  20096  dprd2da  20109  srgdilem  20269  lsssn0  21069  zntoslem  21706  sraassab  22018  blsscls  24664  iimulcl  25096  pi1grplem  25208  pi1xfrf  25212  dvconst  26076  logexprlim  27389  wwlksnextbi  30243  clwwlkccatlem  30340  clwwlkccat  30341  umgr3cyclex  30534  nvss  30945  disjdsct  33048  idlsrgmnd  33804  issgon  34513  measdivcst  34614  measdivcstALTV  34615  prv1n  35923  elmrsubrn  36012  poimirlem28  38319  ftc1anc  38372  fdc  38416  cvrnbtwn3  40070  paddasslem9  40622  paddasslem17  40630  pmapjlln1  40649  lautj  40887  lautm  40888  dfsalgen2  47075  smflimlem4  47508  lidldomnnring  49021  funcringcsetcALTV2lem9  49083  funcringcsetclem9ALTV  49106  lincresunit3lem2  49280  isthincd2  50235