Theorem 3ad2antr2 1206

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3ad2antr2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrl 728	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1188	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

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

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 1103

This theorem is referenced by:  simpr2  1212  simpr2l  1249  simpr2r  1250  simpr21  1277  simpr22  1278  simpr23  1279  wereu  5658  axdc4lem  10438  ioc0  13418  funcestrcsetclem9  18203  funcsetcestrclem9  18218  grpsubadd  19093  unichnlidl  21339  zntoslem  21674  mdsl3  32608  dvrcan5  33495  idlsrgmnd  33748  prv1n  35821  brofs2  36467  brifs2  36468  poimirlem28  38186  ftc1anc  38239  frinfm  38273  welb  38274  fdc  38283  unichnidl  38569  cvrnbtwn2  39938  islpln2a  40211  paddss1  40480  paddss2  40481  paddasslem17  40499  tendospass  41682  funcringcsetcALTV2lem9  48951  funcringcsetclem9ALTV  48974  ldepsprlem  49136