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  5561  funcnvqp  6580  sornom  10230  axdclem2  10473  fzadd2  13520  issubc3  17811  funcestrcsetclem9  18109  funcsetcestrclem9  18124  pgpfi  19535  imasrng  20086  imasring  20239  prdslmodd  20875  icoopnst  24836  iocopnst  24837  axcontlem4  28894  nvmdi  30577  mdsl3  32245  elicc3  36305  iscringd  37992  erngdvlem3  40984  erngdvlem3-rN  40992  dvalveclem  41019  dvhlveclem  41102  dvmptfprodlem  45942  smflimlem4  46772  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309