Theorem 3adantr2 1171

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 593	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  1184  po3nr  5607  funcnvqp  6630  sornom  10317  axdclem2  10560  fzadd2  13599  issubc3  17894  funcestrcsetclem9  18193  funcsetcestrclem9  18208  pgpfi  19623  imasrng  20174  imasring  20327  prdslmodd  20967  icoopnst  24969  iocopnst  24970  axcontlem4  28982  nvmdi  30667  mdsl3  32335  elicc3  36318  iscringd  38005  erngdvlem3  40992  erngdvlem3-rN  41000  dvalveclem  41027  dvhlveclem  41110  dvmptfprodlem  45959  smflimlem4  46789  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237