Theorem 3ad2antr2 1203

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

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

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

This theorem is referenced by:  simpr2  1209  simpr2l  1246  simpr2r  1247  simpr21  1274  simpr22  1275  simpr23  1276  wereu  5643  axdc4lem  10412  ioc0  13396  funcestrcsetclem9  18180  funcsetcestrclem9  18195  grpsubadd  19070  zntoslem  21608  mdsl3  32519  dvrcan5  33416  idlsrgmnd  33710  prv1n  35781  brofs2  36427  brifs2  36428  poimirlem28  38147  ftc1anc  38200  frinfm  38234  welb  38235  fdc  38244  unichnidl  38530  cvrnbtwn2  39899  islpln2a  40172  paddss1  40441  paddss2  40442  paddasslem17  40460  tendospass  41643  funcringcsetcALTV2lem9  48920  funcringcsetclem9ALTV  48943  ldepsprlem  49094