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  5595  dfwe2  7768  smogt  8381  infsupprpr  9518  wlogle  11770  fzadd2  13576  swrdspsleq  14683  tanadd  16185  prdssgrpd  18711  prdsmndd  18748  mhmmnd  19047  imasrng  20137  imasring  20290  prdslmodd  20926  sraassab  21828  mpllsslem  21960  scmatlss  22463  mdetunilem3  22552  ptclsg  23553  tmdgsum2  24034  isxmet2d  24266  xmetres2  24300  prdsxmetlem  24307  comet  24452  iimulcl  24884  icoopnst  24887  iocopnst  24888  icccvx  24899  dvfsumrlim  25990  dvfsumrlim2  25991  colhp  28749  eengtrkg  28965  wwlksnredwwlkn  29877  dmdsl3  32296  eqgvscpbl  33365  resconn  35268  poimirlem28  37672  poimirlem32  37676  broucube  37678  ftc1anclem7  37723  ftc1anc  37725  isdrngo2  37982  iscringd  38022  unichnidl  38055  lplnle  39559  2llnjN  39586  2lplnj  39639  osumcllem11N  39985  cdleme1  40246  erngplus2  40823  erngplus2-rN  40831  erngdvlem3  41009  erngdvlem3-rN  41017  dvaplusgv  41029  dvalveclem  41044  dvhvaddass  41116  dvhlveclem  41127  dihmeetlem12N  41337  issmflem  46756  fmtnoprmfac1  47579  lincresunit3lem2  48456  lincresunit3  48457