MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adantr3 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3simpa 1149 . 2 ((𝜓𝜒𝜏) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 594 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3adant3r3  1185  3ad2antr1  1189  3ad2antr2  1190  sotr2  5575  dfwe2  7699  smogt  8281  infsupprpr  9374  wlogle  11622  fzadd2  13405  swrdspsleq  14485  tanadd  15984  prdsmndd  18524  mhmmnd  18803  imasring  19969  prdslmodd  20354  mpllsslem  21329  scmatlss  21797  mdetunilem3  21886  ptclsg  22889  tmdgsum2  23370  isxmet2d  23603  xmetres2  23637  prdsxmetlem  23644  comet  23792  iimulcl  24223  icoopnst  24225  iocopnst  24226  icccvx  24236  dvfsumrlim  25318  dvfsumrlim2  25319  colhp  27511  eengtrkg  27734  wwlksnredwwlkn  28639  dmdsl3  31056  eqgvscpbl  31936  resconn  33614  poimirlem28  36002  poimirlem32  36006  broucube  36008  ftc1anclem7  36053  ftc1anc  36055  isdrngo2  36313  iscringd  36353  unichnidl  36386  lplnle  37899  2llnjN  37926  2lplnj  37979  osumcllem11N  38325  cdleme1  38586  erngplus2  39163  erngplus2-rN  39171  erngdvlem3  39349  erngdvlem3-rN  39357  dvaplusgv  39369  dvalveclem  39384  dvhvaddass  39456  dvhlveclem  39467  dihmeetlem12N  39677  issmflem  44723  fmtnoprmfac1  45512  lincresunit3lem2  46316  lincresunit3  46317
  Copyright terms: Public domain W3C validator