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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr2  1214  simpr2l  1251  simpr2r  1252  simpr21  1279  simpr22  1280  simpr23  1281  wereu  5647  axdc4lem  10540  ioc0  13530  funcestrcsetclem9  18331  funcsetcestrclem9  18346  grpsubadd  19247  unichnlidl  21525  zntoslem  21871  mdsl3  32927  dvrcan5  33846  idlsrgmnd  34096  prv1n  36314  brofs2  36966  brifs2  36967  poimirlem28  38703  ftc1anc  38756  frinfm  38806  welb  38807  fdc  38816  unichnidl  39102  cvrnbtwn2  40469  islpln2a  40742  paddss1  41011  paddss2  41012  paddasslem17  41030  tendospass  42213  funcringcsetcALTV2lem9  49531  funcringcsetclem9ALTV  49554  ldepsprlem  49720