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  643  tbw-bijust  1535  tbw-negdf  1536  equid  1796  nfdi  1921  hbae  2059  aecom-o  2232  hbae-o  2234  hbequid  2241  equidqe  2254  equid1ALT  2257  axc11nfromc11  2258  ax12inda  2280  vtoclgaf  3169  vtocl2gaf  3171  vtocl3gaf  3173  vtocl4ga  3176  elinti  4280  copsexg  4722  tz7.7  4893  nsuceq0  4947  vtoclr  5033  issref  5368  relresfld  5517  elfvmptrab1  5952  tfisi  6666  bropopvvv  6853  f1o2ndf1  6881  suppimacnv  6902  brovex  6942  tfrlem9  7046  tfrlem11  7049  odi  7220  nndi  7264  sbth  7630  sdomdif  7658  zorn2lem7  8873  alephexp2  8947  addcanpi  9266  mulcanpi  9267  indpi  9274  prcdnq  9360  reclem2pr  9415  lediv2a  10434  nn01to3  11176  brfi1uzind  12516  cshwlen  12761  rlimres  13463  ndvdssub  14149  bitsinv1  14176  nn0seqcvgd  14283  modprm0  14414  initoeu2  15494  symgfixelsi  16659  symgfixfo  16663  uvcendim  19049  slesolex  19351  pm2mpf1  19467  mp2pm2mplem4  19477  fiinopn  19577  jensenlem2  23515  usgraidx2vlem2  24594  wlkcompim  24728  wlkdvspthlem  24811  usgra2adedgspthlem2  24814  clwlkcompim  24966  clwwlknprop  24974  clwlkisclwwlklem2fv2  24985  eleclclwwlkn  25035  hashecclwwlkn1  25036  usghashecclwwlk  25037  clwlkfclwwlk  25046  el2wlkonot  25071  2wlkonot3v  25077  2spthonot3v  25078  3cyclfrgrarn1  25214  3cyclfrgrarn  25215  extwwlkfablem2  25280  numclwlk1lem2foa  25293  frgrareg  25319  clmgmOLD  25521  smgrpmgm  25535  smgrpassOLD  25536  grpomndo  25546  strlem1  27367  ssiun2sf  27636  consym1  30113  zindbi  31121  stoweidlem34  32055  stoweidlem43  32064  funressnfv  32452  funbrafv  32482  ndmaovass  32530  oexpnegALTV  32583  oexpnegnz  32584  ssfz12  32704  usgra2pthlem1  32725  ushguhg  32743  mgm2mgm  32923  exlimexi  33681  eexinst11  33684  e222  33816  e111  33854  eel32131  33903  e333  33924  bnj981  34409  bnj1148  34453  bj-hbaeb2  34792
  Copyright terms: Public domain W3C validator