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 ⊢ (𝜑 → 𝜓)

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  66  impbid  215  anidms  576  tbw-bijust  1726  tbw-negdf  1727  equid  2040  nf5di  2318  hbae  2461  vtoclgaf  3539  vtoclga  3540  elinti  4920  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  vtoclr  5724  ssrelrn  5884  relresfld  6277  tz7.7  6386  elfvunirn  6911  elfvmptrab1  7018  tfisi  7854  bropopvvv  8084  f1o2ndf1  8116  xpord3inddlem  8149  suppimacnv  8169  brovex  8217  tfrlem9  8371  tfrlem11  8374  odi  8563  nndi  8608  sbth  9084  sdomdif  9112  sbthfi  9182  zorn2lem7  10485  alephexp2  10565  addcanpi  10883  mulcanpi  10884  indpi  10891  prcdnq  10977  reclem2pr  11032  lediv2a  12108  nn01to3  12964  fi1uzind  14544  cshwlen  14836  cshwidxmodr  14841  rlimres  15609  ndvdssub  16466  bitsinv1  16499  nn0seqcvgd  16627  modprm0  16864  setsstruct  17235  initoeu2  18072  symgfixelsi  19504  symgfixfo  19508  uvcendim  21976  slesolex  22818  pm2mpf1  22935  mp2pm2mplem4  22945  fiinopn  23037  jensenlem2  27128  umgrupgr  29419  uspgrushgr  29493  uspgrupgr  29494  usgruspgr  29496  usgredg2vlem2  29542  cplgrop  29753  lfgrwlkprop  30001  2pthnloop  30046  usgr2pthlem  30078  elwwlks2  30284  clwlkclwwlklem2fv2  30313  eleclclwwlkn  30393  hashecclwwlkn1  30394  umgrhashecclwwlk  30395  conngrv2edg  30512  3cyclfrgrrn1  30602  l2p  30797  strlem1  32568  ssiun2sf  32870  bnj981  35304  bnj1148  35350  kardfi  35549  swrdrevpfx  35574  consym1  36897  axc11n11  37273  bj-hbaeb2  37419  curryset  37548  currysetlem3  37551  bj-restb  37702  wl-axc11rc11  38204  clmgmOLD  38468  smgrpmgm  38481  smgrpassOLD  38482  grpomndo  38492  eldisjsim3  39554  aecom-o  39643  hbae-o  39645  hbequid  39651  equidqe  39664  equid1ALT  39667  axc11nfromc11  39668  ax12inda  39690  zindbi  43643  sdomne0  44109  exlimexi  45203  eexinst11  45206  e222  45315  e111  45353  e333  45411  stoweidlem34  46718  stoweidlem43  46727  funressnfv  47747  funbrafv  47862  ndmaovass  47910  tz6.12i-afv2  47947  dfatcolem  47959  ssfz12  48018  oexpnegnz  48410  fpprel2  48473  elclnbgrelnbgr  48557  grtriprop  48673  mgm2mgm  48959