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  5547  funcnvqp  6556  sornom  10190  axdclem2  10433  fzadd2  13504  issubc3  17807  funcestrcsetclem9  18105  funcsetcestrclem9  18120  pgpfi  19571  imasrng  20149  imasring  20301  prdslmodd  20955  icoopnst  24916  iocopnst  24917  axcontlem4  29050  nvmdi  30734  mdsl3  32402  elicc3  36515  iscringd  38333  erngdvlem3  41450  erngdvlem3-rN  41458  dvalveclem  41485  dvhlveclem  41568  dvmptfprodlem  46390  smflimlem4  47220  funcringcsetcALTV2lem9  48786  funcringcsetclem9ALTV  48809