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  2011  nf5di  2285  hbae  2435  vtoclgaf  3555  vtoclga  3556  vtocl2gafOLD  3559  vtocl3gafOLD  3561  vtocl3gaOLD  3563  vtocl4gaOLD  3566  elinti  4931  copsexgw  5465  copsexg  5466  vtoclr  5717  ssrelrn  5874  relresfld  6265  tz7.7  6378  elfvunirn  6908  elfvmptrab1  7014  tfisi  7854  bropopvvv  8089  f1o2ndf1  8121  xpord3inddlem  8153  suppimacnv  8173  brovex  8221  tfrlem9  8399  tfrlem11  8402  odi  8591  nndi  8635  sbth  9107  sdomdif  9139  sbthfi  9213  zorn2lem7  10516  alephexp2  10595  addcanpi  10913  mulcanpi  10914  indpi  10921  prcdnq  11007  reclem2pr  11062  lediv2a  12136  nn01to3  12957  fi1uzind  14525  cshwlen  14817  cshwidxmodr  14822  rlimres  15574  ndvdssub  16428  bitsinv1  16461  nn0seqcvgd  16589  modprm0  16825  setsstruct  17195  initoeu2  18029  symgfixelsi  19416  symgfixfo  19420  uvcendim  21807  slesolex  22620  pm2mpf1  22737  mp2pm2mplem4  22747  fiinopn  22839  jensenlem2  26950  umgrupgr  29082  uspgrushgr  29156  uspgrupgr  29157  usgruspgr  29159  usgredg2vlem2  29205  cplgrop  29416  lfgrwlkprop  29667  2pthnloop  29713  usgr2pthlem  29745  elwwlks2  29948  clwlkclwwlklem2fv2  29977  eleclclwwlkn  30057  hashecclwwlkn1  30058  umgrhashecclwwlk  30059  conngrv2edg  30176  3cyclfrgrrn1  30266  l2p  30460  strlem1  32231  ssiun2sf  32540  bnj981  34981  bnj1148  35027  swrdrevpfx  35139  consym1  36438  axc11n11  36700  bj-hbaeb2  36836  curryset  36964  currysetlem3  36967  bj-restb  37112  wl-axc11rc11  37601  clmgmOLD  37875  smgrpmgm  37888  smgrpassOLD  37889  grpomndo  37899  aecom-o  38919  hbae-o  38921  hbequid  38927  equidqe  38940  equid1ALT  38943  axc11nfromc11  38944  ax12inda  38966  zindbi  42970  sdomne0  43437  exlimexi  44549  eexinst11  44552  e222  44661  e111  44699  e333  44757  stoweidlem34  46063  stoweidlem43  46072  funressnfv  47072  funbrafv  47187  ndmaovass  47235  tz6.12i-afv2  47272  dfatcolem  47284  ssfz12  47343  oexpnegnz  47692  fpprel2  47755  elclnbgrelnbgr  47839  grtriprop  47953  mgm2mgm  48202