Theorem 3ad2antr2 1188

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpr2  1194  simpr2l  1231  simpr2r  1232  simpr21  1259  simpr22  1260  simpr23  1261  wereu  5685  axdc4lem  10493  ioc0  13431  funcestrcsetclem9  18204  funcsetcestrclem9  18219  grpsubadd  19059  zntoslem  21593  mdsl3  32345  dvrcan5  33226  idlsrgmnd  33522  prv1n  35416  brofs2  36059  brifs2  36060  poimirlem28  37635  ftc1anc  37688  frinfm  37722  welb  37723  fdc  37732  unichnidl  38018  cvrnbtwn2  39257  islpln2a  39531  paddss1  39800  paddss2  39801  paddasslem17  39819  tendospass  41002  funcringcsetcALTV2lem9  48142  funcringcsetclem9ALTV  48165  ldepsprlem  48318