Theorem 3adantr3 1214

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  3ad2antr1  1218  3ad2antr2  1219  3adant3r3  1267  sotr2  4978  dfwe2  6850  smogt  7328  wlogle  10410  fzadd2  12202  tanadd  14682  prdsmndd  17092  mhmmnd  17306  imasring  18388  prdslmodd  18736  mpllsslem  19202  scmatlss  20092  mdetunilem3  20181  ptclsg  21170  tmdgsum2  21652  isxmet2d  21883  xmetres2  21917  prdsxmetlem  21924  comet  22069  iimulcl  22475  icoopnst  22477  iocopnst  22478  icccvx  22488  dvfsumrlim  23515  dvfsumrlim2  23516  colhp  25380  eengtrkg  25583  wwlknredwwlkn  26020  grponpncan  26550  nvsubadd  26680  dmdsl3  28364  rescon  30288  poimirlem28  32403  poimirlem32  32407  broucube  32409  ftc1anclem7  32457  ftc1anc  32459  isdrngo2  32723  iscringd  32763  unichnidl  32796  lplnle  33640  2llnjN  33667  2lplnj  33720  osumcllem11N  34066  cdleme1  34328  erngplus2  34906  erngplus2-rN  34914  erngdvlem3  35092  erngdvlem3-rN  35100  dvaplusgv  35112  dvalveclem  35128  dvhvaddass  35200  dvhlveclem  35211  dihmeetlem12N  35421  issmflem  39410  fmtnoprmfac1  39813  wwlksnredwwlkn  41096  lincresunit3lem2  42058  lincresunit3  42059