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  5546  funcnvqp  6550  sornom  10190  axdclem2  10433  fzadd2  13481  issubc3  17775  funcestrcsetclem9  18073  funcsetcestrclem9  18088  pgpfi  19503  imasrng  20081  imasring  20234  prdslmodd  20891  icoopnst  24853  iocopnst  24854  axcontlem4  28931  nvmdi  30611  mdsl3  32279  elicc3  36310  iscringd  37997  erngdvlem3  40989  erngdvlem3-rN  40997  dvalveclem  41024  dvhlveclem  41107  dvmptfprodlem  45945  smflimlem4  46775  funcringcsetcALTV2lem9  48302  funcringcsetclem9ALTV  48325