Theorem 3adantr2 1172

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3adant3r2  1191  po3nr  5290  funcnvqp  6200  sornom  9436  axdclem2  9679  fzadd2  12698  issubc3  16905  funcestrcsetclem9  17185  funcsetcestrclem9  17200  pgpfi  18415  imasring  19017  prdslmodd  19375  icoopnst  23157  iocopnst  23158  axcontlem4  26333  nvmdi  28092  mdsl3  29764  elicc3  32908  iscringd  34430  erngdvlem3  37153  erngdvlem3-rN  37161  dvalveclem  37188  dvhlveclem  37271  dvmptfprodlem  41101  smflimlem4  41923  funcringcsetcALTV2lem9  43073  funcringcsetclem9ALTV  43096