Theorem 3ad2antr1 1219

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ispod  4967  funcnvqp  5866  dfwe2  6873  poxp  7176  cfcoflem  8977  axdc3lem  9155  fzadd2  12247  fzosubel2  12395  hashdifpr  13064  sqr0lem  13829  iscatd2  16165  funcestrcsetclem9  16611  funcsetcestrclem9  16626  curf2cl  16694  yonedalem4c  16740  grpsubadd  17326  mulgnnass  17399  mulgnnassOLD  17400  mulgnn0ass  17401  dprdss  18251  dprd2da  18264  srgi  18334  lsssn0  18769  psrbaglesupp  19189  zntoslem  19724  blsscls  22122  iimulcl  22544  pi1grplem  22657  pi1xfrf  22661  dvconst  23486  logexprlim  24750  constr3trllem1  26178  wwlknextbi  26253  nvss  26832  disjdsct  28863  issgon  29513  measdivcstOLD  29614  measdivcst  29615  elmrsubrn  30671  poimirlem28  32607  ftc1anc  32663  fdc  32711  cvrnbtwn3  33581  paddasslem9  34132  paddasslem17  34140  pmapjlln1  34159  lautj  34397  lautm  34398  dfsalgen2  39235  smflimlem4  39660  pfxccat3a  40292  splvalpfx  40298  wwlksnextbi  41100  umgr3cyclex  41350  lidldomnnring  41720  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  lincresunit3lem2  42063