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  5673  axdc4lem  10453  ioc0  13376  funcestrcsetclem9  18105  funcsetcestrclem9  18120  grpsubadd  18948  zntoslem  21332  psrbaglesuppOLD  21698  mdsl3  31833  dvrcan5  32652  idlsrgmnd  32899  prv1n  34717  brofs2  35350  brifs2  35351  poimirlem28  36820  ftc1anc  36873  frinfm  36907  welb  36908  fdc  36917  unichnidl  37203  cvrnbtwn2  38449  islpln2a  38723  paddss1  38992  paddss2  38993  paddasslem17  39011  tendospass  40194  funcringcsetcALTV2lem9  47032  funcringcsetclem9ALTV  47055  ldepsprlem  47242