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

Theorem 3adantr3 1157
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 993 . 2
2 3adantr.1 . 2
31, 2sylan2 474 1
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
  Copyright terms: Public domain W3C validator