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  5627  axdc4lem  10377  ioc0  13345  funcestrcsetclem9  18114  funcsetcestrclem9  18129  grpsubadd  19004  zntoslem  21536  mdsl3  32387  dvrcan5  33297  idlsrgmnd  33574  prv1n  35613  brofs2  36259  brifs2  36260  poimirlem28  37969  ftc1anc  38022  frinfm  38056  welb  38057  fdc  38066  unichnidl  38352  cvrnbtwn2  39721  islpln2a  39994  paddss1  40263  paddss2  40264  paddasslem17  40282  tendospass  41465  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797  ldepsprlem  48948