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  pm2.18OLD  129  impbid  214  anidms  569  tbw-bijust  1699  tbw-negdf  1700  equid  2019  nf5di  2293  hbae  2453  vtoclgaf  3573  vtoclga  3574  vtocl2gaf  3576  vtocl3gaf  3577  vtocl4ga  3580  vtocl2dOLD  3931  elinti  4885  copsexgw  5381  copsexg  5382  vtoclr  5615  ssrelrn  5763  relresfld  6127  tz7.7  6217  elfvmptrab1  6795  tfisi  7573  bropopvvv  7785  f1o2ndf1  7818  suppimacnv  7841  brovex  7888  tfrlem9  8021  tfrlem11  8024  odi  8205  nndi  8249  sbth  8637  sdomdif  8665  zorn2lem7  9924  alephexp2  10003  addcanpi  10321  mulcanpi  10322  indpi  10329  prcdnq  10415  reclem2pr  10470  lediv2a  11534  nn01to3  12342  fi1uzind  13856  cshwlen  14161  cshwidxmodr  14166  rlimres  14915  ndvdssub  15760  bitsinv1  15791  nn0seqcvgd  15914  modprm0  16142  setsstruct  16523  initoeu2  17276  symgfixelsi  18563  symgfixfo  18567  uvcendim  20991  slesolex  21291  pm2mpf1  21407  mp2pm2mplem4  21417  fiinopn  21509  jensenlem2  25565  umgrupgr  26888  uspgrushgr  26960  uspgrupgr  26961  usgruspgr  26963  usgredg2vlem2  27008  cplgrop  27219  lfgrwlkprop  27469  2pthnloop  27512  usgr2pthlem  27544  elwwlks2  27745  clwlkclwwlklem2fv2  27774  eleclclwwlkn  27855  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  conngrv2edg  27974  3cyclfrgrrn1  28064  l2p  28256  strlem1  30027  ssiun2sf  30311  bnj981  32222  bnj1148  32268  swrdrevpfx  32363  consym1  33768  axc11n11  34016  bj-hbaeb2  34141  curryset  34260  currysetlem3  34263  bj-restb  34388  wl-axc11rc11  34830  clmgmOLD  35144  smgrpmgm  35157  smgrpassOLD  35158  grpomndo  35168  aecom-o  36052  hbae-o  36054  hbequid  36060  equidqe  36073  equid1ALT  36076  axc11nfromc11  36077  ax12inda  36099  zindbi  39563  exlimexi  40878  eexinst11  40881  e222  40990  e111  41028  e333  41087  stoweidlem34  42339  stoweidlem43  42348  funressnfv  43298  funbrafv  43377  ndmaovass  43425  tz6.12i-afv2  43462  dfatcolem  43474  ssfz12  43534  oexpnegnz  43863  fpprel2  43926  mgm2mgm  44154