Theorem 3adantr3 1168

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3adant3r3  1181  3ad2antr1  1185  3ad2antr2  1186  sotr2  5469  dfwe2  7476  smogt  7987  infsupprpr  8952  wlogle  11162  fzadd2  12937  swrdspsleq  14018  tanadd  15512  prdsmndd  17936  mhmmnd  18213  imasring  19365  prdslmodd  19734  mpllsslem  20673  scmatlss  21130  mdetunilem3  21219  ptclsg  22220  tmdgsum2  22701  isxmet2d  22934  xmetres2  22968  prdsxmetlem  22975  comet  23120  iimulcl  23542  icoopnst  23544  iocopnst  23545  icccvx  23555  dvfsumrlim  24634  dvfsumrlim2  24635  colhp  26564  eengtrkg  26780  wwlksnredwwlkn  27681  dmdsl3  30098  eqgvscpbl  30970  resconn  32606  poimirlem28  35085  poimirlem32  35089  broucube  35091  ftc1anclem7  35136  ftc1anc  35138  isdrngo2  35396  iscringd  35436  unichnidl  35469  lplnle  36836  2llnjN  36863  2lplnj  36916  osumcllem11N  37262  cdleme1  37523  erngplus2  38100  erngplus2-rN  38108  erngdvlem3  38286  erngdvlem3-rN  38294  dvaplusgv  38306  dvalveclem  38321  dvhvaddass  38393  dvhlveclem  38404  dihmeetlem12N  38614  issmflem  43361  fmtnoprmfac1  44082  lincresunit3lem2  44889  lincresunit3  44890