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, 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 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  640  tbw-bijust  1510  tbw-negdf  1511  equid  1734  nfdi  1853  hbae  2007  aecom-o  2205  hbae-o  2207  hbequid  2214  equidqe  2227  equid1ALT  2230  axc11nfromc11  2231  ax12inda  2253  vtoclgaf  3032  vtocl2gaf  3034  vtocl3gaf  3036  vtocl4ga  3039  elinti  4134  copsexg  4573  copsexgOLD  4574  tz7.7  4741  nsuceq0  4795  vtoclr  4879  issref  5208  relresfld  5361  tfisi  6468  bropopvvv  6652  f1o2ndf1  6679  suppimacnv  6700  brovex  6739  tfrlem9  6840  tfrlem11  6843  odi  7014  nndi  7058  sbth  7427  sdomdif  7455  zorn2lem7  8667  alephexp2  8741  addcanpi  9064  mulcanpi  9065  indpi  9072  prcdnq  9158  reclem2pr  9213  lediv2a  10222  brfi1uzind  12215  cshwlen  12432  rlimres  13032  ndvdssub  13607  bitsinv1  13634  nn0seqcvgd  13741  modprm0  13869  symgfixelsi  15933  symgfixfo  15938  uvcendim  18235  slesolex  18447  fiinopn  18473  jensenlem2  22340  usgraidx2vlem2  23245  wlkdvspthlem  23441  clmgm  23743  smgrpmgm  23757  smgrpass  23758  grpomndo  23768  strlem1  25589  ssiun2sf  25845  consym1  28196  zindbi  29212  stoweidlem34  29754  stoweidlem43  29763  funressnfv  29959  funbrafv  29989  ndmaovass  30037  elfvmptrab1  30079  nn01to3  30112  ssfz12  30122  wlkcompim  30212  usgra2pthlem1  30225  usgra2adedgspthlem2  30229  el2wlkonot  30313  2wlkonot3v  30319  2spthonot3v  30320  clwlkcompim  30352  clwwlknprop  30360  clwlkisclwwlklem2fv2  30370  eleclclwwlkn  30432  hashecclwwlkn1  30433  usghashecclwwlk  30434  clwlkfclwwlk  30442  3cyclfrgrarn1  30529  3cyclfrgrarn  30530  extwwlkfablem2  30596  numclwlk1lem2foa  30609  frgrareg  30635  exlimexi  31062  eexinst11  31065  e222  31192  e111  31230  eel32131  31279  e333  31300  bnj981  31777  bnj1148  31821
  Copyright terms: Public domain W3C validator