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  1701  tbw-negdf  1702  equid  2015  nf5di  2282  hbae  2431  vtoclgaf  3509  vtoclga  3510  vtocl2gaf  3512  vtocl3gaf  3513  vtocl3ga  3514  vtocl4ga  3517  elinti  4888  copsexgw  5402  copsexg  5403  vtoclr  5645  ssrelrn  5796  relresfld  6172  tz7.7  6285  elfvmptrab1  6894  tfisi  7695  bropopvvv  7917  f1o2ndf1  7950  suppimacnv  7977  brovex  8025  tfrlem9  8203  tfrlem11  8206  odi  8397  nndi  8441  sbth  8867  sdomdif  8899  sbthfi  8972  zorn2lem7  10268  alephexp2  10347  addcanpi  10665  mulcanpi  10666  indpi  10673  prcdnq  10759  reclem2pr  10814  lediv2a  11879  nn01to3  12691  fi1uzind  14221  cshwlen  14522  cshwidxmodr  14527  rlimres  15277  ndvdssub  16128  bitsinv1  16159  nn0seqcvgd  16285  modprm0  16516  setsstruct  16887  initoeu2  17741  symgfixelsi  19053  symgfixfo  19057  uvcendim  21064  slesolex  21841  pm2mpf1  21958  mp2pm2mplem4  21968  fiinopn  22060  jensenlem2  26147  umgrupgr  27483  uspgrushgr  27555  uspgrupgr  27556  usgruspgr  27558  usgredg2vlem2  27603  cplgrop  27814  lfgrwlkprop  28064  2pthnloop  28107  usgr2pthlem  28139  elwwlks2  28339  clwlkclwwlklem2fv2  28368  eleclclwwlkn  28448  hashecclwwlkn1  28449  umgrhashecclwwlk  28450  conngrv2edg  28567  3cyclfrgrrn1  28657  l2p  28849  strlem1  30620  ssiun2sf  30907  bnj981  32938  bnj1148  32984  swrdrevpfx  33086  consym1  34617  axc11n11  34872  bj-hbaeb2  35009  curryset  35143  currysetlem3  35146  bj-restb  35273  wl-axc11rc11  35742  clmgmOLD  36017  smgrpmgm  36030  smgrpassOLD  36031  grpomndo  36041  aecom-o  36923  hbae-o  36925  hbequid  36931  equidqe  36944  equid1ALT  36947  axc11nfromc11  36948  ax12inda  36970  zindbi  40776  exlimexi  42125  eexinst11  42128  e222  42237  e111  42275  e333  42334  stoweidlem34  43556  stoweidlem43  43565  funressnfv  44515  funbrafv  44628  ndmaovass  44676  tz6.12i-afv2  44713  dfatcolem  44725  ssfz12  44784  oexpnegnz  45108  fpprel2  45171  mgm2mgm  45399