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

Theorem pm2.43i 43
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 19 . 2  |-  ( ph  ->  ph )
2 pm2.43i.1 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
31, 2mpd 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  sylc  56  pm2.18  102  impbid  183  ibi  232  anidms  626  tbw-bijust  1453  tbw-negdf  1454  equid  1662  hbae  1906  aecom-o  2103  hbae-o  2105  hbequid  2112  equidqe  2125  equid1ALT  2128  ax10from10o  2129  ax11inda  2152  vtoclgaf  2861  vtocl2gaf  2863  vtocl3gaf  2865  elinti  3887  copsexg  4268  tz7.7  4434  nsuceq0  4488  tfisi  4665  vtoclr  4749  issref  5072  relresfld  5215  tfrlem9  6417  tfrlem11  6420  odi  6593  nndi  6637  sbth  6997  sdomdif  7025  zorn2lem7  8145  alephexp2  8219  addcanpi  8539  mulcanpi  8540  indpi  8547  prcdnq  8633  reclem2pr  8688  lediv2a  9666  rlimres  12048  ndvdssub  12622  nn0seqcvgd  12756  fiinopn  16663  jensenlem2  20298  clmgm  21004  smgrpmgm  21018  smgrpass  21019  grpomndo  21029  strlem1  22846  ssiun2sf  23173  fmptcof2  23244  consym1  24931  imgfldref2  25167  inttrp  25211  celsor  25214  eqfnung2  25221  relinccppr  25232  sssu  25244  oriso  25317  preodom2  25329  preoran2  25333  altprs2  25339  int2pre  25340  iscomb  25437  mndoid  25460  mndoio  25461  mndoass  25462  mgmrddd  25469  grpodivone  25476  inttop4  25620  osneisi  25634  limptlimpr2lem2  25678  iintlem1  25713  lvsovso  25729  claddrvr  25751  sigadd  25752  icccon2  25803  morsubc  25958  cmpmor  26078  clscnc  26113  pfsubkl  26150  pgapspf2  26156  isibg2aa  26215  isib2g1a1  26219  isibg1a2  26220  isibg2a  26221  isibg1a3a  26225  isibg1spa  26226  isibg1a5a  26227  isibg1a6  26228  pdiveql  26271  zindbi  27134  stoweidlem4  27856  stoweidlem6  27858  stoweidlem8  27860  stoweidlem20  27872  stoweidlem22  27874  stoweidlem26  27878  stoweidlem27  27879  stoweidlem34  27886  stoweidlem36  27888  stoweidlem43  27895  funressnfv  28096  funbrafv  28126  ndmaovass  28174  brovex  28205  usisuslgra  28247  trlonprop  28341  wlkdvspthlem  28365  3cyclfrgrarn1  28435  3cyclfrgrarn  28436  exlimexi  28586  eexinst11  28589  e222  28713  e111  28751  eel2221  28781  eel32131  28801  eel1111  28809  eel11111  28812  e333  28822  bnj981  29298  bnj1148  29342  hbaewAUX7  29455  hbaew0AUX7  29617  hbaeOLD7  29662  ax9lem1  29762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator