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  5659  axdc4lem  10454  ioc0  13437  funcestrcsetclem9  18228  funcsetcestrclem9  18243  grpsubadd  19140  unichnlidl  21414  zntoslem  21758  mdsl3  32741  dvrcan5  33621  idlsrgmnd  33870  prv1n  35962  brofs2  36608  brifs2  36609  poimirlem28  38358  ftc1anc  38411  frinfm  38446  welb  38447  fdc  38456  unichnidl  38742  cvrnbtwn2  40109  islpln2a  40382  paddss1  40651  paddss2  40652  paddasslem17  40670  tendospass  41853  funcringcsetcALTV2lem9  49122  funcringcsetclem9ALTV  49145  ldepsprlem  49311