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  577  tbw-bijust  1731  tbw-negdf  1732  equid  2045  nf5di  2320  hbae  2462  vtoclgaf  3538  vtoclga  3539  elinti  4919  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  vtoclr  5722  ssrelrn  5882  relresfldOLD  6278  tz7.7  6387  elfvunirn  6912  elfvmptrab1  7019  tfisi  7858  bropopvvv  8090  f1o2ndf1  8122  xpord3inddlem  8155  suppimacnv  8175  brovex  8223  tfrlem9  8377  tfrlem11  8380  odi  8569  nndi  8614  sbth  9098  sdomdif  9126  sbthfi  9196  zorn2lem7  10507  alephexp2  10593  addcanpi  10911  mulcanpi  10912  indpi  10919  prcdnq  11005  reclem2pr  11060  lediv2a  12136  nn01to3  12993  fi1uzind  14574  swrdrevpfx  14840  cshwlen  14872  cshwidxmodr  14877  rlimres  15647  ndvdssub  16503  bitsinv1  16536  nn0seqcvgd  16664  modprm0  16901  setsstruct  17272  initoeu2  18109  symgfixelsi  19566  symgfixfo  19570  uvcendim  22064  slesolex  22911  pm2mpf1  23028  mp2pm2mplem4  23038  fiinopn  23130  jensenlem2  27225  umgrupgr  29561  uspgrushgr  29638  uspgrupgr  29639  usgruspgr  29641  usgredg2vlem2  29687  cplgrop  29898  lfgrwlkprop  30150  2pthnloop  30197  usgr2pthlem  30229  elwwlks2  30438  clwlkclwwlklem2fv2  30467  eleclclwwlkn  30547  hashecclwwlkn1  30548  umgrhashecclwwlk  30549  conngrv2edg  30676  3cyclfrgrrn1  30766  l2p  30961  strlem1  32732  ssiun2sf  33034  bnj981  35461  bnj1148  35507  kardfi  35698  consym1  37041  axc11n11  37417  bj-hbaeb2  37563  curryset  37692  currysetlem3  37695  bj-restb  37846  wl-axc11rc11  38348  clmgmOLD  38603  smgrpmgm  38616  smgrpassOLD  38617  grpomndo  38627  eldisjsim3  39687  aecom-o  39776  hbae-o  39778  hbequid  39784  equidqe  39797  equid1ALT  39800  axc11nfromc11  39801  ax12inda  39823  zindbi  43789  sdomne0  44255  exlimexi  45349  eexinst11  45352  e222  45461  e111  45499  e333  45557  stoweidlem34  46864  stoweidlem43  46873  funressnfv  47933  funbrafv  48048  ndmaovass  48096  tz6.12i-afv2  48133  dfatcolem  48145  ssfz12  48204  oexpnegnz  48596  fpprel2  48659  elclnbgrelnbgr  48743  grtriprop  48859  mgm2mgm  49144