Theorem 3adantr2 1170

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 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3adant3r2  1183  po3nr  5603  funcnvqp  6612  sornom  10271  axdclem2  10514  fzadd2  13535  issubc3  17798  funcestrcsetclem9  18099  funcsetcestrclem9  18114  pgpfi  19472  imasring  20142  prdslmodd  20579  icoopnst  24454  iocopnst  24455  axcontlem4  28222  nvmdi  29896  mdsl3  31564  elicc3  35197  iscringd  36861  erngdvlem3  39856  erngdvlem3-rN  39864  dvalveclem  39891  dvhlveclem  39974  dvmptfprodlem  44650  smflimlem4  45480  imasrng  46668  funcringcsetcALTV2lem9  46932  funcringcsetclem9ALTV  46955