Theorem 3ad2antr1 1195

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpr1  1201  simpr1l  1237  simpr1r  1238  simpr11  1264  simpr12  1265  simpr13  1266  ispod  5535  funcnvqp  6549  dfwe2  7717  poxp  8068  cfcoflem  10185  axdc3lem  10363  fzadd2  13504  fzosubel2  13671  hashdifpr  14368  pfxccat3a  14691  sqrt0  15194  iscatd2  17638  funcestrcsetclem9  18105  funcsetcestrclem9  18120  curf2cl  18188  yonedalem4c  18234  grpsubadd  18995  mulgnnass  19076  mulgnn0ass  19077  dprdss  19997  dprd2da  20010  srgdilem  20164  lsssn0  20938  zntoslem  21531  sraassab  21843  blsscls  24490  iimulcl  24922  pi1grplem  25034  pi1xfrf  25038  dvconst  25902  logexprlim  27206  wwlksnextbi  29980  clwwlkccatlem  30077  clwwlkccat  30078  umgr3cyclex  30271  nvss  30682  disjdsct  32795  idlsrgmnd  33597  issgon  34307  measdivcst  34408  measdivcstALTV  34409  prv1n  35659  elmrsubrn  35748  poimirlem28  38015  ftc1anc  38068  fdc  38112  cvrnbtwn3  39768  paddasslem9  40320  paddasslem17  40328  pmapjlln1  40347  lautj  40585  lautm  40586  dfsalgen2  46784  smflimlem4  47217  lidldomnnring  48727  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812  lincresunit3lem2  48971  isthincd2  49927