Theorem 3ad2antr2 1188

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 206  df-an 396  df-3an 1088

This theorem is referenced by:  simpr2  1194  simpr2l  1231  simpr2r  1232  simpr21  1259  simpr22  1260  simpr23  1261  wereu  5672  axdc4lem  10456  ioc0  13378  funcestrcsetclem9  18110  funcsetcestrclem9  18125  grpsubadd  18954  zntoslem  21423  psrbaglesuppOLD  21789  mdsl3  32004  dvrcan5  32823  idlsrgmnd  33070  prv1n  34888  brofs2  35521  brifs2  35522  poimirlem28  36983  ftc1anc  37036  frinfm  37070  welb  37071  fdc  37080  unichnidl  37366  cvrnbtwn2  38612  islpln2a  38886  paddss1  39155  paddss2  39156  paddasslem17  39174  tendospass  40357  funcringcsetcALTV2lem9  47138  funcringcsetclem9ALTV  47161  ldepsprlem  47318