Theorem 3adantr3 1170

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 1147	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 592	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3r3  1183  3ad2antr1  1187  3ad2antr2  1188  sotr2  5620  dfwe2  7764  smogt  8370  infsupprpr  9502  wlogle  11752  fzadd2  13541  swrdspsleq  14620  tanadd  16115  prdssgrpd  18659  prdsmndd  18693  mhmmnd  18984  imasrng  20072  imasring  20219  prdslmodd  20725  sraassab  21642  mpllsslem  21779  scmatlss  22248  mdetunilem3  22337  ptclsg  23340  tmdgsum2  23821  isxmet2d  24054  xmetres2  24088  prdsxmetlem  24095  comet  24243  iimulcl  24681  icoopnst  24684  iocopnst  24685  icccvx  24696  dvfsumrlim  25784  dvfsumrlim2  25785  colhp  28289  eengtrkg  28512  wwlksnredwwlkn  29417  dmdsl3  31836  eqgvscpbl  32736  resconn  34536  poimirlem28  36820  poimirlem32  36824  broucube  36826  ftc1anclem7  36871  ftc1anc  36873  isdrngo2  37130  iscringd  37170  unichnidl  37203  lplnle  38715  2llnjN  38742  2lplnj  38795  osumcllem11N  39141  cdleme1  39402  erngplus2  39979  erngplus2-rN  39987  erngdvlem3  40165  erngdvlem3-rN  40173  dvaplusgv  40185  dvalveclem  40200  dvhvaddass  40272  dvhlveclem  40283  dihmeetlem12N  40493  issmflem  45742  fmtnoprmfac1  46532  lincresunit3lem2  47249  lincresunit3  47250