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  1662  hbae  1906  aecom-o  2103  hbae-o  2105  hbequid  2112  equidqe  2125  equid1ALT  2128  ax10from10o  2129  ax11inda  2152  vtoclgaf  2861  vtocl2gaf  2863  vtocl3gaf  2865  elinti  3887  copsexg  4268  tz7.7  4434  nsuceq0  4488  tfisi  4665  vtoclr  4749  issref  5072  relresfld  5215  tfrlem9  6417  tfrlem11  6420  odi  6593  nndi  6637  sbth  6997  sdomdif  7025  zorn2lem7  8145  alephexp2  8219  addcanpi  8539  mulcanpi  8540  indpi  8547  prcdnq  8633  reclem2pr  8688  lediv2a  9666  rlimres  12048  ndvdssub  12622  nn0seqcvgd  12756  fiinopn  16663  jensenlem2  20298  clmgm  21004  smgrpmgm  21018  smgrpass  21019  grpomndo  21029  strlem1  22846  ssiun2sf  23173  fmptcof2  23244  consym1  24930  imgfldref2  25166  inttrp  25210  celsor  25213  eqfnung2  25220  relinccppr  25231  sssu  25243  oriso  25316  preodom2  25328  preoran2  25332  altprs2  25338  int2pre  25339  iscomb  25436  mndoid  25459  mndoio  25460  mndoass  25461  mgmrddd  25468  grpodivone  25475  inttop4  25619  osneisi  25633  limptlimpr2lem2  25677  iintlem1  25712  lvsovso  25728  claddrvr  25750  sigadd  25751  icccon2  25802  morsubc  25957  cmpmor  26077  clscnc  26112  pfsubkl  26149  pgapspf2  26155  isibg2aa  26214  isib2g1a1  26218  isibg1a2  26219  isibg2a  26220  isibg1a3a  26224  isibg1spa  26225  isibg1a5a  26226  isibg1a6  26227  pdiveql  26270  zindbi  27133  stoweidlem4  27855  stoweidlem6  27857  stoweidlem8  27859  stoweidlem20  27871  stoweidlem22  27873  stoweidlem26  27877  stoweidlem27  27878  stoweidlem34  27885  stoweidlem36  27887  stoweidlem43  27894  funressnfv  28095  funbrafv  28125  ndmaovass  28173  brovex  28204  usisuslgra  28246  trlonprop  28340  wlkdvspthlem  28364  3cyclfrgrarn1  28434  3cyclfrgrarn  28435  exlimexi  28585  eexinst11  28588  e222  28712  e111  28750  eel2221  28780  eel32131  28800  eel1111  28808  eel11111  28811  e333  28821  bnj981  29297  bnj1148  29341  hbaewAUX7  29454  hbaew0AUX7  29617  hbaeOLD7  29662  ax9lem1  29762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator