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  1644  hbae  1893  aecom-o  2090  hbae-o  2092  hbequid  2099  equidqe  2112  equid1ALT  2115  ax10from10o  2116  ax11inda  2139  vtoclgaf  2848  vtocl2gaf  2850  vtocl3gaf  2852  elinti  3871  copsexg  4252  tz7.7  4418  nsuceq0  4472  tfisi  4649  vtoclr  4733  issref  5056  relresfld  5199  tfrlem9  6401  tfrlem11  6404  odi  6577  nndi  6621  sbth  6981  sdomdif  7009  zorn2lem7  8129  alephexp2  8203  addcanpi  8523  mulcanpi  8524  indpi  8531  prcdnq  8617  reclem2pr  8672  lediv2a  9650  rlimres  12032  ndvdssub  12606  nn0seqcvgd  12740  fiinopn  16647  jensenlem2  20282  clmgm  20988  smgrpmgm  21002  smgrpass  21003  grpomndo  21013  strlem1  22830  ssiun2sf  23157  fmptcof2  23229  consym1  24859  imgfldref2  25064  inttrp  25108  celsor  25111  eqfnung2  25118  relinccppr  25129  sssu  25141  oriso  25214  preodom2  25226  preoran2  25230  altprs2  25236  int2pre  25237  iscomb  25334  mndoid  25357  mndoio  25358  mndoass  25359  mgmrddd  25366  grpodivone  25373  inttop4  25517  osneisi  25531  limptlimpr2lem2  25575  iintlem1  25610  lvsovso  25626  claddrvr  25648  sigadd  25649  icccon2  25700  morsubc  25855  cmpmor  25975  clscnc  26010  pfsubkl  26047  pgapspf2  26053  isibg2aa  26112  isib2g1a1  26116  isibg1a2  26117  isibg2a  26118  isibg1a3a  26122  isibg1spa  26123  isibg1a5a  26124  isibg1a6  26125  pdiveql  26168  zindbi  27031  stoweidlem4  27753  stoweidlem6  27755  stoweidlem8  27757  stoweidlem20  27769  stoweidlem22  27771  stoweidlem26  27775  stoweidlem27  27776  stoweidlem34  27783  stoweidlem36  27785  stoweidlem43  27792  funressnfv  27991  funbrafv  28020  ndmaovass  28066  usisuslgra  28113  exlimexi  28287  eexinst11  28290  e222  28408  e111  28446  eel2221  28476  e333  28508  bnj981  28982  bnj1148  29026  ax9lem1  29140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator