Theorem pm2.43i 53

Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 57. (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 23	. 2 ⊢ (𝜑 → 𝜑)
2		pm2.43i.1	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	1, 2	mpd 16	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  sylc  66  impbid  215  anidms  576  tbw-bijust  1727  tbw-negdf  1728  equid  2041  nf5di  2319  hbae  2462  vtoclgaf  3539  vtoclga  3540  elinti  4920  copsexgw  5471  copsexgwOLD  5472  copsexg  5473  vtoclr  5723  ssrelrn  5883  relresfld  6277  tz7.7  6386  elfvunirn  6911  elfvmptrab1  7018  tfisi  7853  bropopvvv  8083  f1o2ndf1  8115  xpord3inddlem  8148  suppimacnv  8168  brovex  8216  tfrlem9  8370  tfrlem11  8373  odi  8562  nndi  8607  sbth  9083  sdomdif  9111  sbthfi  9181  zorn2lem7  10492  alephexp2  10572  addcanpi  10890  mulcanpi  10891  indpi  10898  prcdnq  10984  reclem2pr  11039  lediv2a  12115  nn01to3  12971  fi1uzind  14551  cshwlen  14843  cshwidxmodr  14848  rlimres  15616  ndvdssub  16473  bitsinv1  16506  nn0seqcvgd  16634  modprm0  16871  setsstruct  17242  initoeu2  18079  symgfixelsi  19511  symgfixfo  19515  uvcendim  22008  slesolex  22850  pm2mpf1  22967  mp2pm2mplem4  22977  fiinopn  23069  jensenlem2  27163  umgrupgr  29464  uspgrushgr  29538  uspgrupgr  29539  usgruspgr  29541  usgredg2vlem2  29587  cplgrop  29798  lfgrwlkprop  30046  2pthnloop  30091  usgr2pthlem  30123  elwwlks2  30329  clwlkclwwlklem2fv2  30358  eleclclwwlkn  30438  hashecclwwlkn1  30439  umgrhashecclwwlk  30440  conngrv2edg  30557  3cyclfrgrrn1  30647  l2p  30842  strlem1  32613  ssiun2sf  32915  bnj981  35347  bnj1148  35393  kardfi  35591  swrdrevpfx  35616  consym1  36959  axc11n11  37335  bj-hbaeb2  37481  curryset  37610  currysetlem3  37613  bj-restb  37764  wl-axc11rc11  38266  clmgmOLD  38530  smgrpmgm  38543  smgrpassOLD  38544  grpomndo  38554  eldisjsim3  39614  aecom-o  39703  hbae-o  39705  hbequid  39711  equidqe  39724  equid1ALT  39727  axc11nfromc11  39728  ax12inda  39750  zindbi  43701  sdomne0  44167  exlimexi  45261  eexinst11  45264  e222  45373  e111  45411  e333  45469  stoweidlem34  46776  stoweidlem43  46785  funressnfv  47808  funbrafv  47923  ndmaovass  47971  tz6.12i-afv2  48008  dfatcolem  48020  ssfz12  48079  oexpnegnz  48471  fpprel2  48534  elclnbgrelnbgr  48618  grtriprop  48734  mgm2mgm  49020