Theorem 3ad2antr2 1186

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpr2  1192  simpr2l  1229  simpr2r  1230  simpr21  1257  simpr22  1258  simpr23  1259  wereu  5520  axdc4lem  9915  ioc0  12826  funcestrcsetclem9  17464  funcsetcestrclem9  17479  grpsubadd  18254  zntoslem  20324  psrbaglesuppOLD  20687  mdsl3  30198  dvrcan5  31016  idlsrgmnd  31180  prv1n  32909  brofs2  33928  brifs2  33929  poimirlem28  35365  ftc1anc  35418  frinfm  35453  welb  35454  fdc  35463  unichnidl  35749  cvrnbtwn2  36851  islpln2a  37124  paddss1  37393  paddss2  37394  paddasslem17  37412  tendospass  38595  funcringcsetcALTV2lem9  45035  funcringcsetclem9ALTV  45058  ldepsprlem  45246