MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43i Structured version   Visualization version   GIF version

Theorem pm2.43i 52
Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 56. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43i.1 (𝜑 → (𝜑𝜓))
Assertion
Ref Expression
pm2.43i (𝜑𝜓)

Proof of Theorem pm2.43i
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 pm2.43i.1 . 2 (𝜑 → (𝜑𝜓))
31, 2mpd 15 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  sylc  65  pm2.18OLD  129  impbid  213  anidms  567  tbw-bijust  1690  tbw-negdf  1691  equid  2010  nf5di  2285  hbae  2448  vtoclgaf  3573  vtoclga  3574  vtocl2gaf  3576  vtocl3gaf  3577  vtocl4ga  3580  vtocl2dOLD  3930  elinti  4878  copsexgw  5373  copsexg  5374  vtoclr  5609  ssrelrn  5757  relresfld  6121  tz7.7  6211  elfvmptrab1  6788  tfisi  7561  bropopvvv  7776  f1o2ndf1  7809  suppimacnv  7832  brovex  7879  tfrlem9  8012  tfrlem11  8015  odi  8195  nndi  8239  sbth  8626  sdomdif  8654  zorn2lem7  9913  alephexp2  9992  addcanpi  10310  mulcanpi  10311  indpi  10318  prcdnq  10404  reclem2pr  10459  lediv2a  11523  nn01to3  12330  fi1uzind  13845  cshwlen  14151  cshwidxmodr  14156  rlimres  14905  ndvdssub  15750  bitsinv1  15781  nn0seqcvgd  15904  modprm0  16132  setsstruct  16513  initoeu2  17266  symgfixelsi  18494  symgfixfo  18498  uvcendim  20921  slesolex  21221  pm2mpf1  21337  mp2pm2mplem4  21347  fiinopn  21439  jensenlem2  25493  umgrupgr  26816  uspgrushgr  26888  uspgrupgr  26889  usgruspgr  26891  usgredg2vlem2  26936  cplgrop  27147  lfgrwlkprop  27397  2pthnloop  27440  usgr2pthlem  27472  elwwlks2  27673  clwlkclwwlklem2fv2  27702  eleclclwwlkn  27783  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  conngrv2edg  27902  3cyclfrgrrn1  27992  l2p  28184  strlem1  29955  ssiun2sf  30240  bnj981  32122  bnj1148  32166  swrdrevpfx  32261  consym1  33666  axc11n11  33914  bj-hbaeb2  34039  curryset  34155  currysetlem3  34158  bj-restb  34280  wl-axc11rc11  34697  clmgmOLD  35012  smgrpmgm  35025  smgrpassOLD  35026  grpomndo  35036  aecom-o  35919  hbae-o  35921  hbequid  35927  equidqe  35940  equid1ALT  35943  axc11nfromc11  35944  ax12inda  35966  zindbi  39423  exlimexi  40738  eexinst11  40741  e222  40850  e111  40888  e333  40947  stoweidlem34  42200  stoweidlem43  42209  funressnfv  43159  funbrafv  43238  ndmaovass  43286  tz6.12i-afv2  43323  dfatcolem  43335  ssfz12  43395  oexpnegnz  43690  fpprel2  43753  mgm2mgm  44032
  Copyright terms: Public domain W3C validator