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  5573  funcnvqp  6605  sornom  10359  axdclem2  10602  fzadd2  13697  issubc3  18030  funcestrcsetclem9  18328  funcsetcestrclem9  18343  pgpfi  19825  imasrng  20405  imasring  20566  prdslmodd  21250  icoopnst  25266  iocopnst  25267  axcontlem4  29551  nvmdi  31256  mdsl3  32924  elicc3  37198  iscringd  39026  erngdvlem3  42141  erngdvlem3-rN  42149  dvalveclem  42176  dvhlveclem  42259  dvmptfprodlem  47048  smflimlem4  47878  funcringcsetcALTV2lem9  49489  funcringcsetclem9ALTV  49512