Theorem 3ad2antr2 1208

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  simpr2  1214  simpr2l  1251  simpr2r  1252  simpr21  1279  simpr22  1280  simpr23  1281  wereu  5657  axdc4lem  10434  ioc0  13414  funcestrcsetclem9  18199  funcsetcestrclem9  18214  grpsubadd  19089  unichnlidl  21362  zntoslem  21706  mdsl3  32668  dvrcan5  33555  idlsrgmnd  33804  prv1n  35923  brofs2  36569  brifs2  36570  poimirlem28  38299  ftc1anc  38352  frinfm  38386  welb  38387  fdc  38396  unichnidl  38682  cvrnbtwn2  40049  islpln2a  40322  paddss1  40591  paddss2  40592  paddasslem17  40610  tendospass  41793  funcringcsetcALTV2lem9  49063  funcringcsetclem9ALTV  49086  ldepsprlem  49252