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  5547  funcnvqp  6556  sornom  10187  axdclem2  10430  fzadd2  13475  issubc3  17773  funcestrcsetclem9  18071  funcsetcestrclem9  18086  pgpfi  19534  imasrng  20112  imasring  20266  prdslmodd  20920  icoopnst  24892  iocopnst  24893  axcontlem4  29040  nvmdi  30723  mdsl3  32391  elicc3  36511  iscringd  38199  erngdvlem3  41250  erngdvlem3-rN  41258  dvalveclem  41285  dvhlveclem  41368  dvmptfprodlem  46188  smflimlem4  47018  funcringcsetcALTV2lem9  48544  funcringcsetclem9ALTV  48567