Theorem 3ad2antr2 1190

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 1172	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  1196  simpr2l  1233  simpr2r  1234  simpr21  1261  simpr22  1262  simpr23  1263  wereu  5615  axdc4lem  10349  ioc0  13295  funcestrcsetclem9  18054  funcsetcestrclem9  18069  grpsubadd  18907  zntoslem  21463  mdsl3  32260  dvrcan5  33176  idlsrgmnd  33451  prv1n  35408  brofs2  36055  brifs2  36056  poimirlem28  37632  ftc1anc  37685  frinfm  37719  welb  37720  fdc  37729  unichnidl  38015  cvrnbtwn2  39258  islpln2a  39531  paddss1  39800  paddss2  39801  paddasslem17  39819  tendospass  41002  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  ldepsprlem  48461