Theorem 3adantr2 1168

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 1147	. 2 ⊢ ((𝜓 ∧ 𝜏 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 592	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3adant3r2  1181  po3nr  5517  funcnvqp  6494  sornom  10017  axdclem2  10260  fzadd2  13273  issubc3  17545  funcestrcsetclem9  17846  funcsetcestrclem9  17861  pgpfi  19191  imasring  19839  prdslmodd  20212  icoopnst  24083  iocopnst  24084  axcontlem4  27316  nvmdi  28989  mdsl3  30657  elicc3  34485  iscringd  36135  erngdvlem3  38983  erngdvlem3-rN  38991  dvalveclem  39018  dvhlveclem  39101  dvmptfprodlem  43439  smflimlem4  44260  funcringcsetcALTV2lem9  45554  funcringcsetclem9ALTV  45577