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  5618  axdc4lem  10363  ioc0  13306  funcestrcsetclem9  18069  funcsetcestrclem9  18084  grpsubadd  18956  zntoslem  21509  mdsl3  32340  dvrcan5  33267  idlsrgmnd  33544  prv1n  35574  brofs2  36220  brifs2  36221  poimirlem28  37788  ftc1anc  37841  frinfm  37875  welb  37876  fdc  37885  unichnidl  38171  cvrnbtwn2  39474  islpln2a  39747  paddss1  40016  paddss2  40017  paddasslem17  40035  tendospass  41218  funcringcsetcALTV2lem9  48486  funcringcsetclem9ALTV  48509  ldepsprlem  48660