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  1697  tbw-negdf  1698  equid  2010  nf5di  2284  hbae  2434  vtoclgaf  3559  vtoclga  3560  vtocl2gafOLD  3563  vtocl3gafOLD  3565  vtocl3gaOLD  3567  vtocl4gaOLD  3570  elinti  4935  copsexgw  5475  copsexg  5476  vtoclr  5728  ssrelrn  5885  relresfld  6276  tz7.7  6389  elfvunirn  6918  elfvmptrab1  7024  tfisi  7862  bropopvvv  8097  f1o2ndf1  8129  xpord3inddlem  8161  suppimacnv  8181  brovex  8229  tfrlem9  8407  tfrlem11  8410  odi  8599  nndi  8643  sbth  9115  sdomdif  9147  sbthfi  9221  zorn2lem7  10524  alephexp2  10603  addcanpi  10921  mulcanpi  10922  indpi  10929  prcdnq  11015  reclem2pr  11070  lediv2a  12144  nn01to3  12965  fi1uzind  14529  cshwlen  14820  cshwidxmodr  14825  rlimres  15577  ndvdssub  16429  bitsinv1  16462  nn0seqcvgd  16590  modprm0  16826  setsstruct  17196  initoeu2  18033  symgfixelsi  19422  symgfixfo  19426  uvcendim  21822  slesolex  22637  pm2mpf1  22754  mp2pm2mplem4  22764  fiinopn  22856  jensenlem2  26968  umgrupgr  29049  uspgrushgr  29123  uspgrupgr  29124  usgruspgr  29126  usgredg2vlem2  29172  cplgrop  29383  lfgrwlkprop  29634  2pthnloop  29680  usgr2pthlem  29712  elwwlks2  29915  clwlkclwwlklem2fv2  29944  eleclclwwlkn  30024  hashecclwwlkn1  30025  umgrhashecclwwlk  30026  conngrv2edg  30143  3cyclfrgrrn1  30233  l2p  30427  strlem1  32198  ssiun2sf  32508  bnj981  34939  bnj1148  34985  swrdrevpfx  35097  consym1  36396  axc11n11  36658  bj-hbaeb2  36794  curryset  36922  currysetlem3  36925  bj-restb  37070  wl-axc11rc11  37559  clmgmOLD  37833  smgrpmgm  37846  smgrpassOLD  37847  grpomndo  37857  aecom-o  38877  hbae-o  38879  hbequid  38885  equidqe  38898  equid1ALT  38901  axc11nfromc11  38902  ax12inda  38924  zindbi  42936  sdomne0  43403  exlimexi  44516  eexinst11  44519  e222  44628  e111  44666  e333  44725  stoweidlem34  46021  stoweidlem43  46030  funressnfv  47028  funbrafv  47143  ndmaovass  47191  tz6.12i-afv2  47228  dfatcolem  47240  ssfz12  47299  oexpnegnz  47638  fpprel2  47701  elclnbgrelnbgr  47785  grtriprop  47881  mgm2mgm  48116