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  5651  axdc4lem  10458  ioc0  13446  funcestrcsetclem9  18237  funcsetcestrclem9  18252  grpsubadd  19152  unichnlidl  21426  zntoslem  21770  mdsl3  32798  dvrcan5  33676  idlsrgmnd  33925  prv1n  36011  brofs2  36658  brifs2  36659  poimirlem28  38398  ftc1anc  38451  frinfm  38486  welb  38487  fdc  38496  unichnidl  38782  cvrnbtwn2  40149  islpln2a  40422  paddss1  40691  paddss2  40692  paddasslem17  40710  tendospass  41893  funcringcsetcALTV2lem9  49214  funcringcsetclem9ALTV  49237  ldepsprlem  49403