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  5564  funcnvqp  6583  sornom  10237  axdclem2  10480  fzadd2  13527  issubc3  17818  funcestrcsetclem9  18116  funcsetcestrclem9  18131  pgpfi  19542  imasrng  20093  imasring  20246  prdslmodd  20882  icoopnst  24843  iocopnst  24844  axcontlem4  28901  nvmdi  30584  mdsl3  32252  elicc3  36312  iscringd  37999  erngdvlem3  40991  erngdvlem3-rN  40999  dvalveclem  41026  dvhlveclem  41109  dvmptfprodlem  45949  smflimlem4  46779  funcringcsetcALTV2lem9  48290  funcringcsetclem9ALTV  48313