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 716	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1171	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  1195  simpr2l  1232  simpr2r  1233  simpr21  1260  simpr22  1261  simpr23  1262  wereu  5661  axdc4lem  10477  ioc0  13416  funcestrcsetclem9  18163  funcsetcestrclem9  18178  grpsubadd  19015  zntoslem  21529  mdsl3  32263  dvrcan5  33179  idlsrgmnd  33477  prv1n  35395  brofs2  36037  brifs2  36038  poimirlem28  37614  ftc1anc  37667  frinfm  37701  welb  37702  fdc  37711  unichnidl  37997  cvrnbtwn2  39235  islpln2a  39509  paddss1  39778  paddss2  39779  paddasslem17  39797  tendospass  40980  funcringcsetcALTV2lem9  48172  funcringcsetclem9ALTV  48195  ldepsprlem  48347