Theorem 3ad2antr2 1208

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr2  1214  simpr2l  1251  simpr2r  1252  simpr21  1279  simpr22  1280  simpr23  1281  wereu  5654  frinf  6316  welb  6317  axdc4lem  10572  ioc0  13563  funcestrcsetclem9  18372  funcsetcestrclem9  18387  grpsubadd  19288  unichnlidl  21567  zntoslem  21917  mdsl3  32975  dvrcan5  33895  idlsrgmnd  34150  prv1n  36404  brofs2  37057  brifs2  37058  poimirlem28  38834  ftc1anc  38887  fdc  38945  unichnidl  39231  cvrnbtwn2  40598  islpln2a  40871  paddss1  41140  paddss2  41141  paddasslem17  41159  tendospass  42342  funcringcsetcALTV2lem9  49668  funcringcsetclem9ALTV  49691  ldepsprlem  49915