Theorem 3ad2antr2 1189

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpr2  1195  simpr2l  1232  simpr2r  1233  simpr21  1260  simpr22  1261  simpr23  1262  wereu  5672  axdc4lem  10449  ioc0  13370  funcestrcsetclem9  18099  funcsetcestrclem9  18114  grpsubadd  18910  zntoslem  21111  psrbaglesuppOLD  21477  mdsl3  31564  dvrcan5  32380  idlsrgmnd  32623  prv1n  34417  brofs2  35044  brifs2  35045  poimirlem28  36511  ftc1anc  36564  frinfm  36598  welb  36599  fdc  36608  unichnidl  36894  cvrnbtwn2  38140  islpln2a  38414  paddss1  38683  paddss2  38684  paddasslem17  38702  tendospass  39885  funcringcsetcALTV2lem9  46932  funcringcsetclem9ALTV  46955  ldepsprlem  47143