Theorem 3ad2antr2 1186

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpr2  1192  simpr2l  1229  simpr2r  1230  simpr21  1257  simpr22  1258  simpr23  1259  wereu  5515  axdc4lem  9866  ioc0  12773  funcestrcsetclem9  17390  funcsetcestrclem9  17405  grpsubadd  18179  zntoslem  20248  psrbaglesupp  20606  mdsl3  30099  dvrcan5  30915  idlsrgmnd  31067  prv1n  32791  brofs2  33651  brifs2  33652  poimirlem28  35085  ftc1anc  35138  frinfm  35173  welb  35174  fdc  35183  unichnidl  35469  cvrnbtwn2  36571  islpln2a  36844  paddss1  37113  paddss2  37114  paddasslem17  37132  tendospass  38315  funcringcsetcALTV2lem9  44668  funcringcsetclem9ALTV  44691  ldepsprlem  44881