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

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

Proof of Theorem pm2.43i
StepHypRef Expression
1 id 23 . 2  |-  ( ph  ->  ph )
2 pm2.43i.1 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
31, 2mpd 15 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  sylc  62  pm2.18  113  impbid  193  ibi  244  anidms  649  tbw-bijust  1577  tbw-negdf  1578  equid  1842  equidOLD  1843  nfdi  1974  hbae  2111  vtoclgaf  3150  vtocl2gaf  3152  vtocl3gaf  3154  vtocl4ga  3157  elinti  4267  copsexg  4707  vtoclr  4899  issref  5233  relresfld  5382  tz7.7  5468  nsuceq0  5522  elfvmptrab1  5986  tfisi  6699  bropopvvv  6887  f1o2ndf1  6915  suppimacnv  6936  brovex  6976  tfrlem9  7111  tfrlem11  7114  odi  7288  nndi  7332  sbth  7698  sdomdif  7726  zorn2lem7  8930  alephexp2  9004  addcanpi  9323  mulcanpi  9324  indpi  9331  prcdnq  9417  reclem2pr  9472  lediv2a  10500  nn01to3  11257  brfi1uzind  12641  cshwlen  12886  rlimres  13600  ndvdssub  14363  bitsinv1  14390  nn0seqcvgd  14500  modprm0  14719  initoeu2  15862  symgfixelsi  17027  symgfixfo  17031  uvcendim  19336  slesolex  19638  pm2mpf1  19754  mp2pm2mplem4  19764  fiinopn  19862  jensenlem2  23778  usgraidx2vlem2  24965  wlkcompim  25099  wlkdvspthlem  25182  usgra2adedgspthlem2  25185  clwlkcompim  25337  clwwlknprop  25345  clwlkisclwwlklem2fv2  25356  eleclclwwlkn  25406  hashecclwwlkn1  25407  usghashecclwwlk  25408  clwlkfclwwlk  25417  el2wlkonot  25442  2wlkonot3v  25448  2spthonot3v  25449  3cyclfrgrarn1  25585  3cyclfrgrarn  25586  extwwlkfablem2  25651  numclwlk1lem2foa  25664  frgrareg  25690  clmgmOLD  25894  smgrpmgm  25908  smgrpassOLD  25909  grpomndo  25919  strlem1  27738  vtocl2d  27944  ssiun2sf  28013  bnj981  29549  bnj1148  29593  consym1  30865  bj-hbaeb2  31171  aecom-o  32180  hbae-o  32182  hbequid  32189  equidqe  32202  equid1ALT  32205  axc11nfromc11  32206  ax12inda  32228  zindbi  35500  exlimexi  36518  eexinst11  36521  e222  36653  e111  36691  eel32131  36740  e333  36760  stoweidlem34  37464  stoweidlem43  37473  funressnfv  38029  funbrafv  38059  ndmaovass  38107  oexpnegALTV  38205  oexpnegnz  38206  ssfz12  38412  usgra2pthlem1  38432  ushguhg  38450  mgm2mgm  38630
  Copyright terms: Public domain W3C validator