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  5637  axdc4lem  10415  ioc0  13360  funcestrcsetclem9  18116  funcsetcestrclem9  18131  grpsubadd  18967  zntoslem  21473  mdsl3  32252  dvrcan5  33194  idlsrgmnd  33492  prv1n  35425  brofs2  36072  brifs2  36073  poimirlem28  37649  ftc1anc  37702  frinfm  37736  welb  37737  fdc  37746  unichnidl  38032  cvrnbtwn2  39275  islpln2a  39549  paddss1  39818  paddss2  39819  paddasslem17  39837  tendospass  41020  funcringcsetcALTV2lem9  48290  funcringcsetclem9ALTV  48313  ldepsprlem  48465