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

Theorem pm2.43i 45
Description: Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by 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 20 . 2  |-  ( ph  ->  ph )
2 pm2.43i.1 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
31, 2mpd 15 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  sylc  58  pm2.18  104  impbid  184  ibi  233  anidms  627  tbw-bijust  1469  tbw-negdf  1470  equid  1684  equidOLD  1685  hbae  2005  aecom-o  2201  hbae-o  2203  hbequid  2210  equidqe  2223  equid1ALT  2226  ax10from10o  2227  ax11inda  2250  vtoclgaf  2976  vtocl2gaf  2978  vtocl3gaf  2980  elinti  4019  copsexg  4402  tz7.7  4567  nsuceq0  4621  tfisi  4797  vtoclr  4881  issref  5206  relresfld  5355  bropopvvv  6385  f1o2ndf1  6413  brovex  6433  tfrlem9  6605  tfrlem11  6608  odi  6781  nndi  6825  sbth  7186  sdomdif  7214  zorn2lem7  8338  alephexp2  8412  addcanpi  8732  mulcanpi  8733  indpi  8740  prcdnq  8826  reclem2pr  8881  lediv2a  9860  brfi1uzind  11670  rlimres  12307  ndvdssub  12882  bitsinv1  12909  nn0seqcvgd  13016  fiinopn  16929  jensenlem2  20779  usgraidx2vlem2  21364  wlkdvspthlem  21560  clmgm  21862  smgrpmgm  21876  smgrpass  21877  grpomndo  21887  strlem1  23706  ssiun2sf  23963  consym1  26074  zindbi  26899  stoweidlem34  27650  stoweidlem43  27659  funressnfv  27859  funbrafv  27889  ndmaovass  27937  ssfz12  27976  usgra2pthlem1  28040  usgra2adedgspthlem2  28044  el2wlkonot  28066  2wlkonot3v  28072  2spthonot3v  28073  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  exlimexi  28319  eexinst11  28322  e222  28446  e111  28484  eel32131  28533  e333  28554  bnj981  29027  bnj1148  29071  hbaewAUX7  29184  hbaew0AUX7  29347  hbaeOLD7  29392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator