Theorem 3adantr2 1166

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adant3r2  1179  po3nr  5488  funcnvqp  6418  sornom  9699  axdclem2  9942  fzadd2  12943  issubc3  17119  funcestrcsetclem9  17398  funcsetcestrclem9  17413  pgpfi  18730  imasring  19369  prdslmodd  19741  icoopnst  23543  iocopnst  23544  axcontlem4  26753  nvmdi  28425  mdsl3  30093  elicc3  33665  iscringd  35291  erngdvlem3  38141  erngdvlem3-rN  38149  dvalveclem  38176  dvhlveclem  38259  dvmptfprodlem  42249  smflimlem4  43070  funcringcsetcALTV2lem9  44335  funcringcsetclem9ALTV  44358