Theorem 3ad2antr2 1185

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 1167	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr2  1191  simpr2l  1228  simpr2r  1229  simpr21  1256  simpr22  1257  simpr23  1258  wereu  5545  axdc4lem  9871  ioc0  12779  funcestrcsetclem9  17392  funcsetcestrclem9  17407  grpsubadd  18181  psrbaglesupp  20142  zntoslem  20697  mdsl3  30087  dvrcan5  30859  prv1n  32673  brofs2  33533  brifs2  33534  poimirlem28  34914  ftc1anc  34969  frinfm  35004  welb  35005  fdc  35014  unichnidl  35303  cvrnbtwn2  36405  islpln2a  36678  paddss1  36947  paddss2  36948  paddasslem17  36966  tendospass  38149  funcringcsetcALTV2lem9  44309  funcringcsetclem9ALTV  44332  ldepsprlem  44521