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

Theorem pm2.43i 50
Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 54. (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 23 . 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  63  pm2.18  114  impbid  194  ibi  245  anidms  650  tbw-bijust  1576  tbw-negdf  1577  equid  1845  equidOLD  1846  nfdi  1977  hbae  2115  vtoclgaf  3150  vtocl2gaf  3152  vtocl3gaf  3154  vtocl4ga  3157  elinti  4270  copsexg  4712  vtoclr  4904  issref  5238  relresfld  5387  tz7.7  5474  nsuceq0  5528  elfvmptrab1  5992  tfisi  6705  bropopvvv  6893  f1o2ndf1  6921  suppimacnv  6942  brovex  6985  tfrlem9  7120  tfrlem11  7123  odi  7297  nndi  7341  sbth  7707  sdomdif  7735  zorn2lem7  8945  alephexp2  9019  addcanpi  9337  mulcanpi  9338  indpi  9345  prcdnq  9431  reclem2pr  9486  lediv2a  10513  nn01to3  11270  fi1uzind  12660  cshwlen  12909  rlimres  13627  ndvdssub  14393  bitsinv1  14421  nn0seqcvgd  14534  modprm0  14761  initoeu2  15916  symgfixelsi  17081  symgfixfo  17085  uvcendim  19409  slesolex  19711  pm2mpf1  19827  mp2pm2mplem4  19837  fiinopn  19935  jensenlem2  23917  usgraidx2vlem2  25123  wlkcompim  25258  wlkdvspthlem  25341  usgra2adedgspthlem2  25344  clwlkcompim  25496  clwwlknprop  25504  clwlkisclwwlklem2fv2  25515  eleclclwwlkn  25565  hashecclwwlkn1  25566  usghashecclwwlk  25567  clwlkfclwwlk  25576  el2wlkonot  25601  2wlkonot3v  25607  2spthonot3v  25608  3cyclfrgrarn1  25744  3cyclfrgrarn  25745  extwwlkfablem2  25810  numclwlk1lem2foa  25823  frgrareg  25849  clmgmOLD  26053  smgrpmgm  26067  smgrpassOLD  26068  grpomndo  26078  strlem1  27907  vtocl2d  28113  ssiun2sf  28182  bnj981  29775  bnj1148  29819  consym1  31091  bj-hbaeb2  31396  aecom-o  32446  hbae-o  32448  hbequid  32455  equidqe  32468  equid1ALT  32471  axc11nfromc11  32472  ax12inda  32494  zindbi  35770  exlimexi  36857  eexinst11  36860  e222  36992  e111  37030  eel32131  37079  e333  37099  stoweidlem34  37841  stoweidlem43  37850  funressnfv  38506  funbrafv  38536  ndmaovass  38584  oexpnegALTV  38682  oexpnegnz  38683  ssfz12  38913  ssrelrn  39004  uspgrushgr  39061  uspgrumgr  39062  usgruspgr  39063  usgridx2vlem2  39091  nbcplgr  39255  cplgrop  39258  usgra2pthlem1  39284  ushguhg  39300  mgm2mgm  39480
  Copyright terms: Public domain W3C validator