Theorem 3adantr2 1189

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 1167	. 2 ⊢ ((𝜓 ∧ 𝜏 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 605	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3r2  1202  po3nr  5574  funcnvqp  6602  sornom  10348  axdclem2  10591  fzadd2  13686  issubc3  18017  funcestrcsetclem9  18315  funcsetcestrclem9  18330  pgpfi  19812  imasrng  20392  imasring  20553  prdslmodd  21237  icoopnst  25253  iocopnst  25254  axcontlem4  29538  nvmdi  31243  mdsl3  32911  elicc3  37085  iscringd  38912  erngdvlem3  42027  erngdvlem3-rN  42035  dvalveclem  42062  dvhlveclem  42145  dvmptfprodlem  46923  smflimlem4  47753  funcringcsetcALTV2lem9  49364  funcringcsetclem9ALTV  49387