Theorem 3adantr2 1167

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3adant3r2  1180  po3nr  5605  funcnvqp  6618  sornom  10307  axdclem2  10550  fzadd2  13576  issubc3  17843  funcestrcsetclem9  18147  funcsetcestrclem9  18162  pgpfi  19577  imasrng  20134  imasring  20283  prdslmodd  20870  icoopnst  24912  iocopnst  24913  axcontlem4  28855  nvmdi  30535  mdsl3  32203  elicc3  35934  iscringd  37604  erngdvlem3  40595  erngdvlem3-rN  40603  dvalveclem  40630  dvhlveclem  40713  dvmptfprodlem  45472  smflimlem4  46302  funcringcsetcALTV2lem9  47548  funcringcsetclem9ALTV  47571