Theorem 3adantr3 1167

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adant3r3  1180  3ad2antr1  1184  3ad2antr2  1185  sotr2  5507  dfwe2  7498  smogt  8006  infsupprpr  8970  wlogle  11175  fzadd2  12945  swrdspsleq  14029  tanadd  15522  prdsmndd  17946  mhmmnd  18223  imasring  19371  prdslmodd  19743  mpllsslem  20217  scmatlss  21136  mdetunilem3  21225  ptclsg  22225  tmdgsum2  22706  isxmet2d  22939  xmetres2  22973  prdsxmetlem  22980  comet  23125  iimulcl  23543  icoopnst  23545  iocopnst  23546  icccvx  23556  dvfsumrlim  24630  dvfsumrlim2  24631  colhp  26558  eengtrkg  26774  wwlksnredwwlkn  27675  dmdsl3  30094  eqgvscpbl  30921  resconn  32495  poimirlem28  34922  poimirlem32  34926  broucube  34928  ftc1anclem7  34975  ftc1anc  34977  isdrngo2  35238  iscringd  35278  unichnidl  35311  lplnle  36678  2llnjN  36705  2lplnj  36758  osumcllem11N  37104  cdleme1  37365  erngplus2  37942  erngplus2-rN  37950  erngdvlem3  38128  erngdvlem3-rN  38136  dvaplusgv  38148  dvalveclem  38163  dvhvaddass  38235  dvhlveclem  38246  dihmeetlem12N  38456  issmflem  43011  fmtnoprmfac1  43734  lincresunit3lem2  44542  lincresunit3  44543