Theorem 3ad2antr2 1185

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr2  1191  simpr2l  1228  simpr2r  1229  simpr21  1256  simpr22  1257  simpr23  1258  wereu  5551  axdc4lem  9877  ioc0  12786  funcestrcsetclem9  17398  funcsetcestrclem9  17413  grpsubadd  18187  psrbaglesupp  20148  zntoslem  20703  mdsl3  30093  dvrcan5  30864  prv1n  32678  brofs2  33538  brifs2  33539  poimirlem28  34935  ftc1anc  34990  frinfm  35025  welb  35026  fdc  35035  unichnidl  35324  cvrnbtwn2  36426  islpln2a  36699  paddss1  36968  paddss2  36969  paddasslem17  36987  tendospass  38170  funcringcsetcALTV2lem9  44335  funcringcsetclem9ALTV  44358  ldepsprlem  44547