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  215  anidms  570  tbw-bijust  1700  tbw-negdf  1701  equid  2019  nf5di  2289  hbae  2442  vtoclgaf  3521  vtoclga  3522  vtocl2gaf  3524  vtocl3gaf  3525  vtocl4ga  3528  vtocl2dOLD  3876  elinti  4847  copsexgw  5346  copsexg  5347  vtoclr  5579  ssrelrn  5727  relresfld  6095  tz7.7  6185  elfvmptrab1  6772  tfisi  7553  bropopvvv  7768  f1o2ndf1  7801  suppimacnv  7824  brovex  7871  tfrlem9  8004  tfrlem11  8007  odi  8188  nndi  8232  sbth  8621  sdomdif  8649  zorn2lem7  9913  alephexp2  9992  addcanpi  10310  mulcanpi  10311  indpi  10318  prcdnq  10404  reclem2pr  10459  lediv2a  11523  nn01to3  12329  fi1uzind  13851  cshwlen  14152  cshwidxmodr  14157  rlimres  14907  ndvdssub  15750  bitsinv1  15781  nn0seqcvgd  15904  modprm0  16132  setsstruct  16515  initoeu2  17268  symgfixelsi  18555  symgfixfo  18559  uvcendim  20536  slesolex  21287  pm2mpf1  21404  mp2pm2mplem4  21414  fiinopn  21506  jensenlem2  25573  umgrupgr  26896  uspgrushgr  26968  uspgrupgr  26969  usgruspgr  26971  usgredg2vlem2  27016  cplgrop  27227  lfgrwlkprop  27477  2pthnloop  27520  usgr2pthlem  27552  elwwlks2  27752  clwlkclwwlklem2fv2  27781  eleclclwwlkn  27861  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  conngrv2edg  27980  3cyclfrgrrn1  28070  l2p  28262  strlem1  30033  ssiun2sf  30323  bnj981  32332  bnj1148  32378  swrdrevpfx  32476  consym1  33881  axc11n11  34129  bj-hbaeb2  34256  curryset  34381  currysetlem3  34384  bj-restb  34509  wl-axc11rc11  34980  clmgmOLD  35289  smgrpmgm  35302  smgrpassOLD  35303  grpomndo  35313  aecom-o  36197  hbae-o  36199  hbequid  36205  equidqe  36218  equid1ALT  36221  axc11nfromc11  36222  ax12inda  36244  zindbi  39887  exlimexi  41230  eexinst11  41233  e222  41342  e111  41380  e333  41439  stoweidlem34  42676  stoweidlem43  42685  funressnfv  43635  funbrafv  43714  ndmaovass  43762  tz6.12i-afv2  43799  dfatcolem  43811  ssfz12  43871  oexpnegnz  44196  fpprel2  44259  mgm2mgm  44487