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  5634  axdc4lem  10408  ioc0  13353  funcestrcsetclem9  18109  funcsetcestrclem9  18124  grpsubadd  18960  zntoslem  21466  mdsl3  32245  dvrcan5  33187  idlsrgmnd  33485  prv1n  35418  brofs2  36065  brifs2  36066  poimirlem28  37642  ftc1anc  37695  frinfm  37729  welb  37730  fdc  37739  unichnidl  38025  cvrnbtwn2  39268  islpln2a  39542  paddss1  39811  paddss2  39812  paddasslem17  39830  tendospass  41013  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  ldepsprlem  48461