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  5581  funcnvqp  6634  sornom  10394  axdclem2  10637  fzadd2  13733  issubc3  18074  funcestrcsetclem9  18372  funcsetcestrclem9  18387  pgpfi  19870  imasrng  20450  imasring  20611  prdslmodd  21295  icoopnst  25315  iocopnst  25316  axcontlem4  29602  nvmdi  31307  mdsl3  32975  elicc3  37320  iscringd  39198  erngdvlem3  42313  erngdvlem3-rN  42321  dvalveclem  42348  dvhlveclem  42431  dvmptfprodlem  47227  smflimlem4  48057  funcringcsetcALTV2lem9  49668  funcringcsetclem9ALTV  49691