Theorem 3adantr2 1183

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3adant3r2  1196  po3nr  5566  funcnvqp  6580  sornom  10228  axdclem2  10471  fzadd2  13558  issubc3  17873  funcestrcsetclem9  18171  funcsetcestrclem9  18186  pgpfi  19636  imasrng  20214  imasring  20366  prdslmodd  21024  icoopnst  24989  iocopnst  24990  axcontlem4  29125  nvmdi  30808  mdsl3  32476  elicc3  36638  iscringd  38458  erngdvlem3  41575  erngdvlem3-rN  41583  dvalveclem  41610  dvhlveclem  41693  dvmptfprodlem  46479  smflimlem4  47309  funcringcsetcALTV2lem9  48881  funcringcsetclem9ALTV  48904