Theorem 3adantr2 1171

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

Ref	Expression
3adantr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3adantr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adantr2

Step	Hyp	Ref	Expression
1		3simpb 1149	. 2 ⊢ ((𝜓 ∧ 𝜏 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 593	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:  3adant3r2  1184  po3nr  5576  funcnvqp  6600  sornom  10291  axdclem2  10534  fzadd2  13576  issubc3  17862  funcestrcsetclem9  18160  funcsetcestrclem9  18175  pgpfi  19586  imasrng  20137  imasring  20290  prdslmodd  20926  icoopnst  24887  iocopnst  24888  axcontlem4  28946  nvmdi  30629  mdsl3  32297  elicc3  36335  iscringd  38022  erngdvlem3  41009  erngdvlem3-rN  41017  dvalveclem  41044  dvhlveclem  41127  dvmptfprodlem  45973  smflimlem4  46803  funcringcsetcALTV2lem9  48273  funcringcsetclem9ALTV  48296