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  211  anidms  567  tbw-bijust  1700  tbw-negdf  1701  equid  2015  nf5di  2281  hbae  2429  vtoclgaf  3534  vtoclga  3535  vtocl2gaf  3537  vtocl3gaf  3538  vtocl3ga  3539  vtocl4ga  3542  elinti  4921  copsexgw  5452  copsexg  5453  vtoclr  5700  ssrelrn  5855  relresfld  6233  tz7.7  6348  elfvunirn  6879  elfvmptrab1  6980  tfisi  7800  bropopvvv  8027  f1o2ndf1  8059  xpord3inddlem  8091  suppimacnv  8110  brovex  8158  tfrlem9  8336  tfrlem11  8339  odi  8531  nndi  8575  sbth  9044  sdomdif  9076  sbthfi  9153  zorn2lem7  10447  alephexp2  10526  addcanpi  10844  mulcanpi  10845  indpi  10852  prcdnq  10938  reclem2pr  10993  lediv2a  12058  nn01to3  12875  fi1uzind  14408  cshwlen  14699  cshwidxmodr  14704  rlimres  15452  ndvdssub  16302  bitsinv1  16333  nn0seqcvgd  16457  modprm0  16688  setsstruct  17059  initoeu2  17916  symgfixelsi  19231  symgfixfo  19235  uvcendim  21290  slesolex  22068  pm2mpf1  22185  mp2pm2mplem4  22195  fiinopn  22287  jensenlem2  26374  umgrupgr  28117  uspgrushgr  28189  uspgrupgr  28190  usgruspgr  28192  usgredg2vlem2  28237  cplgrop  28448  lfgrwlkprop  28698  2pthnloop  28742  usgr2pthlem  28774  elwwlks2  28974  clwlkclwwlklem2fv2  29003  eleclclwwlkn  29083  hashecclwwlkn1  29084  umgrhashecclwwlk  29085  conngrv2edg  29202  3cyclfrgrrn1  29292  l2p  29484  strlem1  31255  ssiun2sf  31545  bnj981  33651  bnj1148  33697  swrdrevpfx  33797  consym1  34968  axc11n11  35223  bj-hbaeb2  35359  curryset  35490  currysetlem3  35493  bj-restb  35638  wl-axc11rc11  36108  clmgmOLD  36383  smgrpmgm  36396  smgrpassOLD  36397  grpomndo  36407  aecom-o  37436  hbae-o  37438  hbequid  37444  equidqe  37457  equid1ALT  37460  axc11nfromc11  37461  ax12inda  37483  zindbi  41328  sdomne0  41807  exlimexi  42928  eexinst11  42931  e222  43040  e111  43078  e333  43137  stoweidlem34  44395  stoweidlem43  44404  funressnfv  45397  funbrafv  45510  ndmaovass  45558  tz6.12i-afv2  45595  dfatcolem  45607  ssfz12  45666  oexpnegnz  45990  fpprel2  46053  mgm2mgm  46281