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  5586  funcnvqp  6604  sornom  10272  axdclem2  10515  fzadd2  13599  issubc3  17923  funcestrcsetclem9  18221  funcsetcestrclem9  18236  pgpfi  19698  imasrng  20278  imasring  20437  prdslmodd  21119  icoopnst  25127  iocopnst  25128  axcontlem4  29346  nvmdi  31029  mdsl3  32697  elicc3  36861  iscringd  38682  erngdvlem3  41797  erngdvlem3-rN  41805  dvalveclem  41832  dvhlveclem  41915  dvmptfprodlem  46691  smflimlem4  47521  funcringcsetcALTV2lem9  49096  funcringcsetclem9ALTV  49119