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  2430  vtoclgaf  3564  vtoclga  3565  vtocl2gaf  3567  vtocl3gaf  3568  vtocl3ga  3569  vtocl4ga  3572  elinti  4959  copsexgw  5490  copsexg  5491  vtoclr  5739  ssrelrn  5894  relresfld  6275  tz7.7  6390  elfvunirn  6923  elfvmptrab1  7025  tfisi  7850  bropopvvv  8078  f1o2ndf1  8110  xpord3inddlem  8142  suppimacnv  8161  brovex  8209  tfrlem9  8387  tfrlem11  8390  odi  8581  nndi  8625  sbth  9095  sdomdif  9127  sbthfi  9204  zorn2lem7  10499  alephexp2  10578  addcanpi  10896  mulcanpi  10897  indpi  10904  prcdnq  10990  reclem2pr  11045  lediv2a  12112  nn01to3  12929  fi1uzind  14462  cshwlen  14753  cshwidxmodr  14758  rlimres  15506  ndvdssub  16356  bitsinv1  16387  nn0seqcvgd  16511  modprm0  16742  setsstruct  17113  initoeu2  17970  symgfixelsi  19344  symgfixfo  19348  uvcendim  21621  slesolex  22404  pm2mpf1  22521  mp2pm2mplem4  22531  fiinopn  22623  jensenlem2  26716  umgrupgr  28618  uspgrushgr  28690  uspgrupgr  28691  usgruspgr  28693  usgredg2vlem2  28738  cplgrop  28949  lfgrwlkprop  29199  2pthnloop  29243  usgr2pthlem  29275  elwwlks2  29475  clwlkclwwlklem2fv2  29504  eleclclwwlkn  29584  hashecclwwlkn1  29585  umgrhashecclwwlk  29586  conngrv2edg  29703  3cyclfrgrrn1  29793  l2p  29987  strlem1  31758  ssiun2sf  32046  bnj981  34247  bnj1148  34293  swrdrevpfx  34393  consym1  35608  axc11n11  35863  bj-hbaeb2  35999  curryset  36130  currysetlem3  36133  bj-restb  36278  wl-axc11rc11  36748  clmgmOLD  37022  smgrpmgm  37035  smgrpassOLD  37036  grpomndo  37046  aecom-o  38074  hbae-o  38076  hbequid  38082  equidqe  38095  equid1ALT  38098  axc11nfromc11  38099  ax12inda  38121  zindbi  41987  sdomne0  42466  exlimexi  43587  eexinst11  43590  e222  43699  e111  43737  e333  43796  stoweidlem34  45049  stoweidlem43  45058  funressnfv  46052  funbrafv  46165  ndmaovass  46213  tz6.12i-afv2  46250  dfatcolem  46262  ssfz12  46321  oexpnegnz  46645  fpprel2  46708  mgm2mgm  46904