MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43i Unicode version

Theorem pm2.43i 47
Description: Inference absorbing redundant antecedent. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43i.1
Assertion
Ref Expression
pm2.43i

Proof of Theorem pm2.43i
StepHypRef Expression
1 id 22 . 2
2 pm2.43i.1 . 2
31, 2mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  sylc  60  pm2.18  110  impbid  191  ibi  241  anidms  645  tbw-bijust  1531  tbw-negdf  1532  equid  1791  nfdi  1916  hbae  2055  aecom-o  2230  hbae-o  2232  hbequid  2239  equidqe  2252  equid1ALT  2255  axc11nfromc11  2256  ax12inda  2278  vtoclgaf  3172  vtocl2gaf  3174  vtocl3gaf  3176  vtocl4ga  3179  elinti  4295  copsexg  4737  copsexgOLD  4738  tz7.7  4909  nsuceq0  4963  vtoclr  5049  issref  5385  relresfld  5539  elfvmptrab1  5976  tfisi  6693  bropopvvv  6880  f1o2ndf1  6908  suppimacnv  6929  brovex  6969  tfrlem9  7073  tfrlem11  7076  odi  7247  nndi  7291  sbth  7657  sdomdif  7685  zorn2lem7  8903  alephexp2  8977  addcanpi  9298  mulcanpi  9299  indpi  9306  prcdnq  9392  reclem2pr  9447  lediv2a  10464  nn01to3  11204  brfi1uzind  12532  cshwlen  12770  rlimres  13381  ndvdssub  14065  bitsinv1  14092  nn0seqcvgd  14199  modprm0  14330  symgfixelsi  16460  symgfixfo  16464  uvcendim  18882  slesolex  19184  pm2mpf1  19300  mp2pm2mplem4  19310  fiinopn  19410  jensenlem2  23317  usgraidx2vlem2  24392  wlkcompim  24526  wlkdvspthlem  24609  usgra2adedgspthlem2  24612  clwlkcompim  24764  clwwlknprop  24772  clwlkisclwwlklem2fv2  24783  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlkfclwwlk  24844  el2wlkonot  24869  2wlkonot3v  24875  2spthonot3v  24876  3cyclfrgrarn1  25012  3cyclfrgrarn  25013  extwwlkfablem2  25078  numclwlk1lem2foa  25091  frgrareg  25117  clmgmOLD  25323  smgrpmgm  25337  smgrpassOLD  25338  grpomndo  25348  strlem1  27169  ssiun2sf  27427  consym1  29885  zindbi  30882  stoweidlem34  31816  stoweidlem43  31825  funressnfv  32213  funbrafv  32243  ndmaovass  32291  ssfz12  32330  usgra2pthlem1  32353  ushguhg  32371  mgm2mgm  32551  initoeu2  32622  exlimexi  33294  eexinst11  33297  e222  33422  e111  33460  eel32131  33509  e333  33530  bnj981  34008  bnj1148  34052  bj-hbaeb2  34391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator