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  1683  equidOLD  1684  hbae  2002  aecom-o  2187  hbae-o  2189  hbequid  2196  equidqe  2209  equid1ALT  2212  ax10from10o  2213  ax11inda  2236  vtoclgaf  2961  vtocl2gaf  2963  vtocl3gaf  2965  elinti  4003  copsexg  4385  tz7.7  4550  nsuceq0  4604  tfisi  4780  vtoclr  4864  issref  5189  relresfld  5338  bropopvvv  6367  brovex  6412  tfrlem9  6584  tfrlem11  6587  odi  6760  nndi  6804  sbth  7165  sdomdif  7193  zorn2lem7  8317  alephexp2  8391  addcanpi  8711  mulcanpi  8712  indpi  8719  prcdnq  8805  reclem2pr  8860  lediv2a  9838  brfi1uzind  11644  rlimres  12281  ndvdssub  12856  bitsinv1  12883  nn0seqcvgd  12990  fiinopn  16899  jensenlem2  20695  usgraidx2vlem2  21279  wlkdvspthlem  21457  clmgm  21759  smgrpmgm  21773  smgrpass  21774  grpomndo  21784  strlem1  23603  ssiun2sf  23856  consym1  25886  zindbi  26702  stoweidlem34  27453  stoweidlem43  27462  funressnfv  27663  funbrafv  27693  ndmaovass  27741  3cyclfrgrarn1  27767  3cyclfrgrarn  27768  exlimexi  27953  eexinst11  27956  e222  28080  e111  28118  eel32131  28167  e333  28188  bnj981  28661  bnj1148  28705  hbaewAUX7  28818  hbaew0AUX7  28981  hbaeOLD7  29026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator