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  1518  tbw-negdf  1519  equid  1777  nfdi  1902  hbae  2041  aecom-o  2216  hbae-o  2218  hbequid  2225  equidqe  2238  equid1ALT  2241  axc11nfromc11  2242  ax12inda  2264  vtoclgaf  3158  vtocl2gaf  3160  vtocl3gaf  3162  vtocl4ga  3165  elinti  4280  copsexg  4722  copsexgOLD  4723  tz7.7  4894  nsuceq0  4948  vtoclr  5034  issref  5370  relresfld  5524  elfvmptrab1  5961  tfisi  6678  bropopvvv  6865  f1o2ndf1  6893  suppimacnv  6914  brovex  6952  tfrlem9  7056  tfrlem11  7059  odi  7230  nndi  7274  sbth  7639  sdomdif  7667  zorn2lem7  8885  alephexp2  8959  addcanpi  9280  mulcanpi  9281  indpi  9288  prcdnq  9374  reclem2pr  9429  lediv2a  10445  nn01to3  11184  brfi1uzind  12511  cshwlen  12749  rlimres  13360  ndvdssub  13942  bitsinv1  13969  nn0seqcvgd  14076  modprm0  14207  symgfixelsi  16334  symgfixfo  16338  uvcendim  18755  slesolex  19057  pm2mpf1  19173  mp2pm2mplem4  19183  fiinopn  19283  jensenlem2  23189  usgraidx2vlem2  24264  wlkcompim  24398  wlkdvspthlem  24481  usgra2adedgspthlem2  24484  clwlkcompim  24636  clwwlknprop  24644  clwlkisclwwlklem2fv2  24655  eleclclwwlkn  24705  hashecclwwlkn1  24706  usghashecclwwlk  24707  clwlkfclwwlk  24716  el2wlkonot  24741  2wlkonot3v  24747  2spthonot3v  24748  3cyclfrgrarn1  24884  3cyclfrgrarn  24885  extwwlkfablem2  24950  numclwlk1lem2foa  24963  frgrareg  24989  clmgmOLD  25195  smgrpmgm  25209  smgrpassOLD  25210  grpomndo  25220  strlem1  27041  ssiun2sf  27299  consym1  29860  zindbi  30857  stoweidlem34  31705  stoweidlem43  31714  funressnfv  32051  funbrafv  32081  ndmaovass  32129  ssfz12  32168  usgra2pthlem1  32191  ushguhg  32209  mgm2mgm  32388  exlimexi  33022  eexinst11  33025  e222  33150  e111  33188  eel32131  33237  e333  33258  bnj981  33736  bnj1148  33780  bj-hbaeb2  34133
  Copyright terms: Public domain W3C validator