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  2318  hbae  2460  vtoclgaf  3535  vtoclga  3536  elinti  4915  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  vtoclr  5710  ssrelrn  5872  relresfldOLD  6268  tz7.7  6377  elfvunirn  6903  elfvmptrab1  7010  tfisi  7853  bropopvvv  8084  f1o2ndf1  8116  xpord3inddlem  8149  suppimacnv  8169  brovex  8217  tfrlem9  8371  tfrlem11  8374  odi  8565  nndi  8610  sbth  9094  sdomdif  9122  sbthfi  9192  zorn2lem7  10552  alephexp2  10638  addcanpi  10956  mulcanpi  10957  indpi  10964  prcdnq  11050  reclem2pr  11105  lediv2a  12181  nn01to3  13038  fi1uzind  14620  swrdrevpfx  14886  cshwlen  14918  cshwidxmodr  14923  rlimres  15693  ndvdssub  16547  bitsinv1  16580  nn0seqcvgd  16708  modprm0  16945  setsstruct  17316  initoeu2  18153  symgfixelsi  19611  symgfixfo  19615  uvcendim  22115  slesolex  22962  pm2mpf1  23079  mp2pm2mplem4  23089  fiinopn  23181  jensenlem2  27279  umgrupgr  29615  uspgrushgr  29692  uspgrupgr  29693  usgruspgr  29695  usgredg2vlem2  29741  cplgrop  29952  lfgrwlkprop  30204  2pthnloop  30251  usgr2pthlem  30283  elwwlks2  30492  clwlkclwwlklem2fv2  30521  eleclclwwlkn  30601  hashecclwwlkn1  30602  umgrhashecclwwlk  30603  conngrv2edg  30730  3cyclfrgrrn1  30820  l2p  31015  strlem1  32786  ssiun2sf  33088  bnj981  35515  bnj1148  35561  kardfi  35763  consym1  37130  axc11n11  37506  bj-hbaeb2  37652  curryset  37781  currysetlem3  37784  bj-restb  37935  wl-axc11rc11  38435  clmgmOLD  38705  smgrpmgm  38718  smgrpassOLD  38719  grpomndo  38729  eldisjsim3  39789  aecom-o  39878  hbae-o  39880  hbequid  39886  equidqe  39899  equid1ALT  39902  axc11nfromc11  39903  ax12inda  39925  zindbi  43891  sdomne0  44357  exlimexi  45451  eexinst11  45454  e222  45563  e111  45601  e333  45659  stoweidlem34  46966  stoweidlem43  46975  funressnfv  48035  funbrafv  48150  ndmaovass  48198  tz6.12i-afv2  48235  dfatcolem  48247  ssfz12  48306  oexpnegnz  48698  fpprel2  48761  elclnbgrelnbgr  48845  grtriprop  48961  mgm2mgm  49246