Theorem 3adantr3 1190

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

Ref	Expression
3adantr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3adantr3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3adantr3

Step	Hyp	Ref	Expression
1		3simpa 1166	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 605	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3r3  1203  3ad2antr1  1207  3ad2antr2  1208  sotr2  5592  dfwe2  7788  smogt  8378  infsupprpr  9501  wlogle  11852  fzadd2  13696  swrdspsleq  14819  tanadd  16340  prdssgrpd  18927  prdsmndd  18969  mhmmnd  19279  imasrng  20404  imasring  20565  prdslmodd  21249  sraassab  22181  mpllsslem  22312  scmatlss  22845  mdetunilem3  22934  ptclsg  23939  tmdgsum2  24420  isxmet2d  24651  xmetres2  24685  prdsxmetlem  24692  comet  24837  iimulcl  25263  icoopnst  25265  iocopnst  25266  icccvx  25276  dvfsumrlim  26356  dvfsumrlim2  26357  colhp  29253  eengtrkg  29569  wwlksnredwwlkn  30489  dmdsl3  32922  eqgvscpbl  33957  resconn  36097  poimirlem28  38659  poimirlem32  38663  broucube  38665  ftc1anclem7  38710  ftc1anc  38712  isdrngo2  38985  iscringd  39025  unichnidl  39058  lplnle  40690  2llnjN  40717  2lplnj  40770  osumcllem11N  41116  cdleme1  41377  erngplus2  41954  erngplus2-rN  41962  erngdvlem3  42140  erngdvlem3-rN  42148  dvaplusgv  42160  dvalveclem  42175  dvhvaddass  42247  dvhlveclem  42258  dihmeetlem12N  42468  issmflem  47830  fmtnoprmfac1  48743  lincresunit3lem2  49685  lincresunit3  49686