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  5627  axdc4lem  10384  ioc0  13329  funcestrcsetclem9  18089  funcsetcestrclem9  18104  grpsubadd  18942  zntoslem  21498  mdsl3  32295  dvrcan5  33203  idlsrgmnd  33478  prv1n  35411  brofs2  36058  brifs2  36059  poimirlem28  37635  ftc1anc  37688  frinfm  37722  welb  37723  fdc  37732  unichnidl  38018  cvrnbtwn2  39261  islpln2a  39535  paddss1  39804  paddss2  39805  paddasslem17  39823  tendospass  41006  funcringcsetcALTV2lem9  48279  funcringcsetclem9ALTV  48302  ldepsprlem  48454