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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adant3r2  1184  po3nr  5544  funcnvqp  6553  sornom  10179  axdclem2  10422  fzadd2  13466  issubc3  17764  funcestrcsetclem9  18062  funcsetcestrclem9  18077  pgpfi  19525  imasrng  20103  imasring  20257  prdslmodd  20911  icoopnst  24883  iocopnst  24884  axcontlem4  28966  nvmdi  30649  mdsl3  32317  elicc3  36433  iscringd  38111  erngdvlem3  41162  erngdvlem3-rN  41170  dvalveclem  41197  dvhlveclem  41280  dvmptfprodlem  46104  smflimlem4  46934  funcringcsetcALTV2lem9  48460  funcringcsetclem9ALTV  48483