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  5561  dfwe2  7713  smogt  8293  infsupprpr  9397  wlogle  11657  fzadd2  13461  swrdspsleq  14575  tanadd  16078  prdssgrpd  18643  prdsmndd  18680  mhmmnd  18979  imasrng  20097  imasring  20250  prdslmodd  20904  sraassab  21807  mpllsslem  21938  scmatlss  22441  mdetunilem3  22530  ptclsg  23531  tmdgsum2  24012  isxmet2d  24243  xmetres2  24277  prdsxmetlem  24284  comet  24429  iimulcl  24861  icoopnst  24864  iocopnst  24865  icccvx  24876  dvfsumrlim  25966  dvfsumrlim2  25967  colhp  28749  eengtrkg  28966  wwlksnredwwlkn  29875  dmdsl3  32297  eqgvscpbl  33322  resconn  35311  poimirlem28  37709  poimirlem32  37713  broucube  37715  ftc1anclem7  37760  ftc1anc  37762  isdrngo2  38019  iscringd  38059  unichnidl  38092  lplnle  39660  2llnjN  39687  2lplnj  39740  osumcllem11N  40086  cdleme1  40347  erngplus2  40924  erngplus2-rN  40932  erngdvlem3  41110  erngdvlem3-rN  41118  dvaplusgv  41130  dvalveclem  41145  dvhvaddass  41217  dvhlveclem  41228  dihmeetlem12N  41438  issmflem  46850  fmtnoprmfac1  47690  lincresunit3lem2  48606  lincresunit3  48607