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  5554  funcnvqp  6564  sornom  10206  axdclem2  10449  fzadd2  13496  issubc3  17787  funcestrcsetclem9  18085  funcsetcestrclem9  18100  pgpfi  19511  imasrng  20062  imasring  20215  prdslmodd  20851  icoopnst  24812  iocopnst  24813  axcontlem4  28870  nvmdi  30550  mdsl3  32218  elicc3  36278  iscringd  37965  erngdvlem3  40957  erngdvlem3-rN  40965  dvalveclem  40992  dvhlveclem  41075  dvmptfprodlem  45915  smflimlem4  46745  funcringcsetcALTV2lem9  48259  funcringcsetclem9ALTV  48282