Theorem 3adantr2 1187

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adant3r2  1200  po3nr  5585  funcnvqp  6601  sornom  10261  axdclem2  10504  fzadd2  13587  issubc3  17906  funcestrcsetclem9  18204  funcsetcestrclem9  18219  pgpfi  19675  imasrng  20255  imasring  20412  prdslmodd  21068  icoopnst  25067  iocopnst  25068  axcontlem4  29258  nvmdi  30941  mdsl3  32609  elicc3  36751  iscringd  38572  erngdvlem3  41689  erngdvlem3-rN  41697  dvalveclem  41724  dvhlveclem  41807  dvmptfprodlem  46585  smflimlem4  47415  funcringcsetcALTV2lem9  48987  funcringcsetclem9ALTV  49010