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

 Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 973 This theorem is referenced by:  3ad2antr1  1161  3ad2antr2  1162  3adant3r3  1207  sotr2  4834  dfwe2  6617  smogt  7057  wlogle  10111  tanadd  13902  prdsmndd  15953  mhmmnd  16192  imasring  17268  prdslmodd  17615  mpllsslem  18094  mpllsslemOLD  18096  scmatlss  19027  mdetunilem3  19116  ptclsg  20116  tmdgsum2  20595  isxmet2d  20830  xmetres2  20864  prdsxmetlem  20871  comet  21016  iimulcl  21437  icoopnst  21439  iocopnst  21440  icccvx  21450  dvfsumrlim  22432  dvfsumrlim2  22433  eengtrkg  24288  wwlknredwwlkn  24726  grponpncan  25257  nvsubadd  25550  dmdsl3  27234  rescon  28691  ftc1anclem7  30096  ftc1anc  30098  fzadd2  30234  isdrngo2  30361  iscringd  30396  unichnidl  30428  lincresunit3lem2  33081  lincresunit3  33082  lplnle  35264  2llnjN  35291  2lplnj  35344  osumcllem11N  35690  cdleme1  35952  erngplus2  36530  erngplus2-rN  36538  erngdvlem3  36716  erngdvlem3-rN  36724  dvaplusgv  36736  dvalveclem  36752  dvhvaddass  36824  dvhlveclem  36835  dihmeetlem12N  37045 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 185  df-an 371  df-3an 975