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  5509  funcnvqp  6482  sornom  9964  axdclem2  10207  fzadd2  13220  issubc3  17480  funcestrcsetclem9  17781  funcsetcestrclem9  17796  pgpfi  19125  imasring  19773  prdslmodd  20146  icoopnst  24008  iocopnst  24009  axcontlem4  27238  nvmdi  28911  mdsl3  30579  elicc3  34433  iscringd  36083  erngdvlem3  38931  erngdvlem3-rN  38939  dvalveclem  38966  dvhlveclem  39049  dvmptfprodlem  43375  smflimlem4  44196  funcringcsetcALTV2lem9  45490  funcringcsetclem9ALTV  45513