Theorem 3ad2antr2 1196

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpr2  1202  simpr2l  1239  simpr2r  1240  simpr21  1267  simpr22  1268  simpr23  1269  wereu  5614  axdc4lem  10368  ioc0  13336  funcestrcsetclem9  18105  funcsetcestrclem9  18120  grpsubadd  18995  zntoslem  21531  mdsl3  32405  dvrcan5  33317  idlsrgmnd  33597  prv1n  35659  brofs2  36305  brifs2  36306  poimirlem28  38015  ftc1anc  38068  frinfm  38102  welb  38103  fdc  38112  unichnidl  38398  cvrnbtwn2  39767  islpln2a  40040  paddss1  40309  paddss2  40310  paddasslem17  40328  tendospass  41511  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812  ldepsprlem  48963