Theorem 3ad2antr2 1220

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  wereu  5034  axdc4lem  9160  ioc0  12093  funcestrcsetclem9  16611  funcsetcestrclem9  16626  grpsubadd  17326  psrbaglesupp  19189  zntoslem  19724  trcfilu  21908  constr2wlk  26128  constr2trl  26129  constr3trllem1  26178  mdsl3  28559  dvrcan5  29124  brofs2  31354  brifs2  31355  poimirlem28  32607  ftc1anc  32663  frinfm  32700  welb  32701  fdc  32711  unichnidl  33000  cvrnbtwn2  33580  islpln2a  33852  paddss1  34121  paddss2  34122  paddasslem17  34140  tendospass  35326  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  ldepsprlem  42055