Theorem 3ad2antr1 1168

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simpr1  1174  simpr1l  1210  simpr1r  1211  simpr11  1237  simpr12  1238  simpr13  1239  ispod  5327  funcnvqp  6245  dfwe2  7306  poxp  7620  cfcoflem  9484  axdc3lem  9662  fzadd2  12751  fzosubel2  12905  hashdifpr  13580  pfxccat3a  13932  sqr0lem  14451  iscatd2  16800  funcestrcsetclem9  17246  funcsetcestrclem9  17261  curf2cl  17329  yonedalem4c  17375  grpsubadd  17964  mulgnnass  18036  mulgnn0ass  18037  dprdss  18891  dprd2da  18904  srgi  18974  lsssn0  19431  psrbaglesupp  19852  zntoslem  20395  blsscls  22810  iimulcl  23234  pi1grplem  23346  pi1xfrf  23350  dvconst  24207  logexprlim  25493  wwlksnextbi  27372  wwlksnextbiOLD  27373  umgr3cyclex  27702  nvss  28137  disjdsct  30179  issgon  30984  measdivcstOLD  31085  measdivcst  31086  elmrsubrn  32227  poimirlem28  34309  ftc1anc  34364  fdc  34410  cvrnbtwn3  35805  paddasslem9  36357  paddasslem17  36365  pmapjlln1  36384  lautj  36622  lautm  36623  dfsalgen2  42001  smflimlem4  42427  lidldomnnring  43505  funcringcsetcALTV2lem9  43619  funcringcsetclem9ALTV  43642  lincresunit3lem2  43842