Theorem 3ad2antr2 1191

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpr2  1197  simpr2l  1234  simpr2r  1235  simpr21  1262  simpr22  1263  simpr23  1264  wereu  5621  axdc4lem  10371  ioc0  13339  funcestrcsetclem9  18108  funcsetcestrclem9  18123  grpsubadd  18998  zntoslem  21549  mdsl3  32405  dvrcan5  33315  idlsrgmnd  33592  prv1n  35632  brofs2  36278  brifs2  36279  poimirlem28  37986  ftc1anc  38039  frinfm  38073  welb  38074  fdc  38083  unichnidl  38369  cvrnbtwn2  39738  islpln2a  40011  paddss1  40280  paddss2  40281  paddasslem17  40299  tendospass  41482  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812  ldepsprlem  48963