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  1997  aecom-o  2185  hbae-o  2187  hbequid  2194  equidqe  2207  equid1ALT  2210  ax10from10o  2211  ax11inda  2234  vtoclgaf  2959  vtocl2gaf  2961  vtocl3gaf  2963  elinti  4001  copsexg  4383  tz7.7  4548  nsuceq0  4602  tfisi  4778  vtoclr  4862  issref  5187  relresfld  5336  bropopvvv  6365  brovex  6410  tfrlem9  6582  tfrlem11  6585  odi  6758  nndi  6802  sbth  7163  sdomdif  7191  zorn2lem7  8315  alephexp2  8389  addcanpi  8709  mulcanpi  8710  indpi  8717  prcdnq  8803  reclem2pr  8858  lediv2a  9836  brfi1uzind  11642  rlimres  12279  ndvdssub  12854  bitsinv1  12881  nn0seqcvgd  12988  fiinopn  16897  jensenlem2  20693  usgraidx2vlem2  21277  wlkdvspthlem  21455  clmgm  21757  smgrpmgm  21771  smgrpass  21772  grpomndo  21782  strlem1  23601  ssiun2sf  23854  consym1  25884  zindbi  26700  stoweidlem34  27451  stoweidlem43  27460  funressnfv  27661  funbrafv  27691  ndmaovass  27739  3cyclfrgrarn1  27765  3cyclfrgrarn  27766  exlimexi  27951  eexinst11  27954  e222  28078  e111  28116  eel32131  28165  e333  28186  bnj981  28659  bnj1148  28703  hbaewAUX7  28816  hbaew0AUX7  28979  hbaeOLD7  29024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator