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  1505  tbw-negdf  1506  equid  1729  nfdi  1849  hbae  2002  aecom-o  2201  hbae-o  2203  hbequid  2210  equidqe  2223  equid1ALT  2226  axc11nfromc11  2227  ax12inda  2249  vtoclgaf  3038  vtocl2gaf  3040  vtocl3gaf  3042  vtocl4ga  3045  elinti  4140  copsexg  4579  copsexgOLD  4580  tz7.7  4748  nsuceq0  4802  vtoclr  4886  issref  5214  relresfld  5367  tfisi  6472  bropopvvv  6656  f1o2ndf1  6683  suppimacnv  6704  brovex  6743  tfrlem9  6847  tfrlem11  6850  odi  7021  nndi  7065  sbth  7434  sdomdif  7462  zorn2lem7  8674  alephexp2  8748  addcanpi  9071  mulcanpi  9072  indpi  9079  prcdnq  9165  reclem2pr  9220  lediv2a  10229  brfi1uzind  12222  cshwlen  12439  rlimres  13039  ndvdssub  13614  bitsinv1  13641  nn0seqcvgd  13748  modprm0  13876  symgfixelsi  15943  symgfixfo  15948  uvcendim  18279  slesolex  18491  fiinopn  18517  jensenlem2  22384  usgraidx2vlem2  23313  wlkdvspthlem  23509  clmgm  23811  smgrpmgm  23825  smgrpass  23826  grpomndo  23836  strlem1  25657  ssiun2sf  25913  consym1  28269  zindbi  29290  stoweidlem34  29832  stoweidlem43  29841  funressnfv  30037  funbrafv  30067  ndmaovass  30115  elfvmptrab1  30157  nn01to3  30190  ssfz12  30200  wlkcompim  30290  usgra2pthlem1  30303  usgra2adedgspthlem2  30307  el2wlkonot  30391  2wlkonot3v  30397  2spthonot3v  30398  clwlkcompim  30430  clwwlknprop  30438  clwlkisclwwlklem2fv2  30448  eleclclwwlkn  30510  hashecclwwlkn1  30511  usghashecclwwlk  30512  clwlkfclwwlk  30520  3cyclfrgrarn1  30607  3cyclfrgrarn  30608  extwwlkfablem2  30674  numclwlk1lem2foa  30687  frgrareg  30713  mp2pm2mplem4  30922  pmattomply1f1  30925  exlimexi  31232  eexinst11  31235  e222  31361  e111  31399  eel32131  31448  e333  31469  bnj981  31946  bnj1148  31990
  Copyright terms: Public domain W3C validator