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  5647  axdc4lem  10533  ioc0  13523  funcestrcsetclem9  18322  funcsetcestrclem9  18337  grpsubadd  19238  unichnlidl  21516  zntoslem  21862  mdsl3  32918  dvrcan5  33796  idlsrgmnd  34046  prv1n  36196  brofs2  36842  brifs2  36843  poimirlem28  38566  ftc1anc  38619  frinfm  38669  welb  38670  fdc  38679  unichnidl  38965  cvrnbtwn2  40332  islpln2a  40605  paddss1  40874  paddss2  40875  paddasslem17  40893  tendospass  42076  funcringcsetcALTV2lem9  49394  funcringcsetclem9ALTV  49417  ldepsprlem  49583