Theorem 3adantr3 1172

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 1148	. 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:  3adant3r3  1185  3ad2antr1  1189  3ad2antr2  1190  sotr2  5580  dfwe2  7750  smogt  8336  infsupprpr  9457  wlogle  11711  fzadd2  13520  swrdspsleq  14630  tanadd  16135  prdssgrpd  18660  prdsmndd  18697  mhmmnd  18996  imasrng  20086  imasring  20239  prdslmodd  20875  sraassab  21777  mpllsslem  21909  scmatlss  22412  mdetunilem3  22501  ptclsg  23502  tmdgsum2  23983  isxmet2d  24215  xmetres2  24249  prdsxmetlem  24256  comet  24401  iimulcl  24833  icoopnst  24836  iocopnst  24837  icccvx  24848  dvfsumrlim  25938  dvfsumrlim2  25939  colhp  28697  eengtrkg  28913  wwlksnredwwlkn  29825  dmdsl3  32244  eqgvscpbl  33321  resconn  35233  poimirlem28  37642  poimirlem32  37646  broucube  37648  ftc1anclem7  37693  ftc1anc  37695  isdrngo2  37952  iscringd  37992  unichnidl  38025  lplnle  39534  2llnjN  39561  2lplnj  39614  osumcllem11N  39960  cdleme1  40221  erngplus2  40798  erngplus2-rN  40806  erngdvlem3  40984  erngdvlem3-rN  40992  dvaplusgv  41004  dvalveclem  41019  dvhvaddass  41091  dvhlveclem  41102  dihmeetlem12N  41312  issmflem  46725  fmtnoprmfac1  47566  lincresunit3lem2  48469  lincresunit3  48470