Theorem 3adantr2 1170

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 592	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adant3r2  1183  po3nr  5623  funcnvqp  6642  sornom  10346  axdclem2  10589  fzadd2  13619  issubc3  17913  funcestrcsetclem9  18217  funcsetcestrclem9  18232  pgpfi  19647  imasrng  20204  imasring  20353  prdslmodd  20990  icoopnst  24988  iocopnst  24989  axcontlem4  29000  nvmdi  30680  mdsl3  32348  elicc3  36283  iscringd  37958  erngdvlem3  40947  erngdvlem3-rN  40955  dvalveclem  40982  dvhlveclem  41065  dvmptfprodlem  45865  smflimlem4  46695  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044