MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43i Structured version   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  |-  ( ph  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
pm2.43i  |-  ( ph  ->  ps )

Proof of Theorem pm2.43i
StepHypRef Expression
1 id 22 . 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  60  pm2.18  110  impbid  191  ibi  241  anidms  645  tbw-bijust  1510  tbw-negdf  1511  equid  1735  nfdi  1858  hbae  2021  aecom-o  2216  hbae-o  2218  hbequid  2225  equidqe  2238  equid1ALT  2241  axc11nfromc11  2242  ax12inda  2264  vtoclgaf  3169  vtocl2gaf  3171  vtocl3gaf  3173  vtocl4ga  3176  elinti  4284  copsexg  4725  copsexgOLD  4726  tz7.7  4897  nsuceq0  4951  vtoclr  5036  issref  5371  relresfld  5525  elfvmptrab1  5961  tfisi  6664  bropopvvv  6853  f1o2ndf1  6881  suppimacnv  6902  brovex  6940  tfrlem9  7044  tfrlem11  7047  odi  7218  nndi  7262  sbth  7627  sdomdif  7655  zorn2lem7  8871  alephexp2  8945  addcanpi  9266  mulcanpi  9267  indpi  9274  prcdnq  9360  reclem2pr  9415  lediv2a  10428  nn01to3  11164  brfi1uzind  12485  cshwlen  12720  rlimres  13330  ndvdssub  13913  bitsinv1  13940  nn0seqcvgd  14047  modprm0  14178  symgfixelsi  16248  symgfixfo  16253  uvcendim  18642  slesolex  18944  pm2mpf1  19060  mp2pm2mplem4  19070  fiinopn  19170  jensenlem2  23038  usgraidx2vlem2  24054  wlkcompim  24188  wlkdvspthlem  24271  usgra2adedgspthlem2  24274  clwlkcompim  24426  clwwlknprop  24434  clwlkisclwwlklem2fv2  24445  eleclclwwlkn  24495  hashecclwwlkn1  24496  usghashecclwwlk  24497  clwlkfclwwlk  24506  el2wlkonot  24531  2wlkonot3v  24537  2spthonot3v  24538  3cyclfrgrarn1  24674  3cyclfrgrarn  24675  extwwlkfablem2  24741  numclwlk1lem2foa  24754  frgrareg  24780  clmgm  24985  smgrpmgm  24999  smgrpass  25000  grpomndo  25010  strlem1  26831  ssiun2sf  27086  consym1  29448  zindbi  30473  stoweidlem34  31289  stoweidlem43  31298  funressnfv  31635  funbrafv  31665  ndmaovass  31713  ssfz12  31754  usgra2pthlem1  31777  exlimexi  32248  eexinst11  32251  e222  32377  e111  32415  eel32131  32464  e333  32485  bnj981  32962  bnj1148  33006  bj-hbaeb2  33347
  Copyright terms: Public domain W3C validator