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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		pm2.43i.1	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	1, 2	mpd 15	1 ⊢ (𝜑 → 𝜓)

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  impbid  212  anidms  566  tbw-bijust  1698  tbw-negdf  1699  equid  2012  nf5di  2285  hbae  2429  vtoclgaf  3533  vtoclga  3534  vtocl2gafOLD  3537  vtocl3gafOLD  3539  vtocl3gaOLD  3541  vtocl4gaOLD  3544  elinti  4908  copsexgw  5437  copsexg  5438  vtoclr  5686  ssrelrn  5841  relresfld  6228  tz7.7  6337  elfvunirn  6856  elfvmptrab1  6962  tfisi  7799  bropopvvv  8030  f1o2ndf1  8062  xpord3inddlem  8094  suppimacnv  8114  brovex  8162  tfrlem9  8314  tfrlem11  8317  odi  8504  nndi  8548  sbth  9021  sdomdif  9049  sbthfi  9123  zorn2lem7  10415  alephexp2  10494  addcanpi  10812  mulcanpi  10813  indpi  10820  prcdnq  10906  reclem2pr  10961  lediv2a  12037  nn01to3  12860  fi1uzind  14432  cshwlen  14723  cshwidxmodr  14728  rlimres  15483  ndvdssub  16338  bitsinv1  16371  nn0seqcvgd  16499  modprm0  16735  setsstruct  17105  initoeu2  17941  symgfixelsi  19332  symgfixfo  19336  uvcendim  21772  slesolex  22585  pm2mpf1  22702  mp2pm2mplem4  22712  fiinopn  22804  jensenlem2  26914  umgrupgr  29066  uspgrushgr  29140  uspgrupgr  29141  usgruspgr  29143  usgredg2vlem2  29189  cplgrop  29400  lfgrwlkprop  29649  2pthnloop  29694  usgr2pthlem  29726  elwwlks2  29929  clwlkclwwlklem2fv2  29958  eleclclwwlkn  30038  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  conngrv2edg  30157  3cyclfrgrrn1  30247  l2p  30441  strlem1  32212  ssiun2sf  32521  bnj981  34916  bnj1148  34962  swrdrevpfx  35089  consym1  36393  axc11n11  36655  bj-hbaeb2  36791  curryset  36919  currysetlem3  36922  bj-restb  37067  wl-axc11rc11  37556  clmgmOLD  37830  smgrpmgm  37843  smgrpassOLD  37844  grpomndo  37854  aecom-o  38879  hbae-o  38881  hbequid  38887  equidqe  38900  equid1ALT  38903  axc11nfromc11  38904  ax12inda  38926  zindbi  42919  sdomne0  43386  exlimexi  44498  eexinst11  44501  e222  44610  e111  44648  e333  44706  stoweidlem34  46016  stoweidlem43  46025  funressnfv  47028  funbrafv  47143  ndmaovass  47191  tz6.12i-afv2  47228  dfatcolem  47240  ssfz12  47299  oexpnegnz  47663  fpprel2  47726  elclnbgrelnbgr  47810  grtriprop  47924  mgm2mgm  48199