Theorem 3adantr2 1172

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 594	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  1185  po3nr  5554  funcnvqp  6562  sornom  10199  axdclem2  10442  fzadd2  13513  issubc3  17816  funcestrcsetclem9  18114  funcsetcestrclem9  18129  pgpfi  19580  imasrng  20158  imasring  20310  prdslmodd  20964  icoopnst  24906  iocopnst  24907  axcontlem4  29036  nvmdi  30719  mdsl3  32387  elicc3  36499  iscringd  38319  erngdvlem3  41436  erngdvlem3-rN  41444  dvalveclem  41471  dvhlveclem  41554  dvmptfprodlem  46372  smflimlem4  47202  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797