Theorem 3ad2antr2 1189

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  simpr2  1195  simpr2l  1232  simpr2r  1233  simpr21  1260  simpr22  1261  simpr23  1262  wereu  5672  axdc4lem  10452  ioc0  13373  funcestrcsetclem9  18102  funcsetcestrclem9  18117  grpsubadd  18913  zntoslem  21118  psrbaglesuppOLD  21484  mdsl3  31607  dvrcan5  32426  idlsrgmnd  32673  prv1n  34491  brofs2  35118  brifs2  35119  poimirlem28  36602  ftc1anc  36655  frinfm  36689  welb  36690  fdc  36699  unichnidl  36985  cvrnbtwn2  38231  islpln2a  38505  paddss1  38774  paddss2  38775  paddasslem17  38793  tendospass  39976  funcringcsetcALTV2lem9  47021  funcringcsetclem9ALTV  47044  ldepsprlem  47231