MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43i Structured version   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  1472  tbw-negdf  1473  equid  1688  equidOLD  1689  hbae  2040  hbaeOLD  2041  aecom-o  2227  hbae-o  2229  hbequid  2236  equidqe  2249  equid1ALT  2252  ax10from10o  2253  ax11inda  2276  vtoclgaf  3008  vtocl2gaf  3010  vtocl3gaf  3012  elinti  4051  copsexg  4434  tz7.7  4599  nsuceq0  4653  tfisi  4830  vtoclr  4914  issref  5239  relresfld  5388  bropopvvv  6418  f1o2ndf1  6446  brovex  6466  tfrlem9  6638  tfrlem11  6641  odi  6814  nndi  6858  sbth  7219  sdomdif  7247  zorn2lem7  8374  alephexp2  8448  addcanpi  8768  mulcanpi  8769  indpi  8776  prcdnq  8862  reclem2pr  8917  lediv2a  9896  brfi1uzind  11707  rlimres  12344  ndvdssub  12919  bitsinv1  12946  nn0seqcvgd  13053  fiinopn  16966  jensenlem2  20818  usgraidx2vlem2  21403  wlkdvspthlem  21599  clmgm  21901  smgrpmgm  21915  smgrpass  21916  grpomndo  21926  strlem1  23745  ssiun2sf  24002  consym1  26162  zindbi  27000  stoweidlem34  27750  stoweidlem43  27759  funressnfv  27959  funbrafv  27989  ndmaovass  28037  ssfz12  28088  modprm0  28194  cshw1v  28239  usgra2pthlem1  28263  usgra2adedgspthlem2  28267  el2wlkonot  28289  2wlkonot3v  28295  2spthonot3v  28296  3cyclfrgrarn1  28339  3cyclfrgrarn  28340  exlimexi  28545  eexinst11  28548  e222  28674  e111  28712  eel32131  28761  e333  28782  bnj981  29258  bnj1148  29302  hbaewAUX7  29415  hbaew0AUX7  29584  hbaeOLD7  29645
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator