Theorem 3adantr2 1172

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant3r2  1185  po3nr  5555  funcnvqp  6564  sornom  10199  axdclem2  10442  fzadd2  13487  issubc3  17785  funcestrcsetclem9  18083  funcsetcestrclem9  18098  pgpfi  19546  imasrng  20124  imasring  20278  prdslmodd  20932  icoopnst  24904  iocopnst  24905  axcontlem4  29052  nvmdi  30735  mdsl3  32403  elicc3  36530  iscringd  38246  erngdvlem3  41363  erngdvlem3-rN  41371  dvalveclem  41398  dvhlveclem  41481  dvmptfprodlem  46299  smflimlem4  47129  funcringcsetcALTV2lem9  48655  funcringcsetclem9ALTV  48678