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  5628  axdc4lem  10377  ioc0  13320  funcestrcsetclem9  18083  funcsetcestrclem9  18098  grpsubadd  18970  zntoslem  21523  mdsl3  32404  dvrcan5  33330  idlsrgmnd  33607  prv1n  35647  brofs2  36293  brifs2  36294  poimirlem28  37899  ftc1anc  37952  frinfm  37986  welb  37987  fdc  37996  unichnidl  38282  cvrnbtwn2  39651  islpln2a  39924  paddss1  40193  paddss2  40194  paddasslem17  40212  tendospass  41395  funcringcsetcALTV2lem9  48658  funcringcsetclem9ALTV  48681  ldepsprlem  48832