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

Theorem 3adantr3 1163
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 1140 . 2 ((𝜓𝜒𝜏) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 592 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3adant3r3  1176  3ad2antr1  1180  3ad2antr2  1181  sotr2  5498  dfwe2  7485  smogt  7993  infsupprpr  8956  wlogle  11161  fzadd2  12930  swrdspsleq  14015  tanadd  15508  prdsmndd  17932  mhmmnd  18159  imasring  19298  prdslmodd  19670  mpllsslem  20143  scmatlss  21062  mdetunilem3  21151  ptclsg  22151  tmdgsum2  22632  isxmet2d  22864  xmetres2  22898  prdsxmetlem  22905  comet  23050  iimulcl  23468  icoopnst  23470  iocopnst  23471  icccvx  23481  dvfsumrlim  24555  dvfsumrlim2  24556  colhp  26483  eengtrkg  26699  wwlksnredwwlkn  27600  dmdsl3  30019  eqgvscpbl  30846  resconn  32390  poimirlem28  34801  poimirlem32  34805  broucube  34807  ftc1anclem7  34854  ftc1anc  34856  isdrngo2  35117  iscringd  35157  unichnidl  35190  lplnle  36556  2llnjN  36583  2lplnj  36636  osumcllem11N  36982  cdleme1  37243  erngplus2  37820  erngplus2-rN  37828  erngdvlem3  38006  erngdvlem3-rN  38014  dvaplusgv  38026  dvalveclem  38041  dvhvaddass  38113  dvhlveclem  38124  dihmeetlem12N  38334  issmflem  42881  fmtnoprmfac1  43604  lincresunit3lem2  44463  lincresunit3  44464
  Copyright terms: Public domain W3C validator