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  212  anidms  566  tbw-bijust  1700  tbw-negdf  1701  equid  2014  nf5di  2292  hbae  2436  vtoclgaf  3520  vtoclga  3521  vtocl2gafOLD  3524  vtocl3gafOLD  3526  vtocl3gaOLD  3528  vtocl4gaOLD  3531  elinti  4899  copsexgw  5444  copsexgwOLD  5445  copsexg  5446  vtoclr  5694  ssrelrn  5850  relresfld  6241  tz7.7  6350  elfvunirn  6871  elfvmptrab1  6977  tfisi  7810  bropopvvv  8040  f1o2ndf1  8072  xpord3inddlem  8104  suppimacnv  8124  brovex  8172  tfrlem9  8324  tfrlem11  8327  odi  8514  nndi  8559  sbth  9035  sdomdif  9063  sbthfi  9133  zorn2lem7  10424  alephexp2  10504  addcanpi  10822  mulcanpi  10823  indpi  10830  prcdnq  10916  reclem2pr  10971  lediv2a  12050  nn01to3  12891  fi1uzind  14469  cshwlen  14761  cshwidxmodr  14766  rlimres  15520  ndvdssub  16378  bitsinv1  16411  nn0seqcvgd  16539  modprm0  16776  setsstruct  17146  initoeu2  17983  symgfixelsi  19410  symgfixfo  19414  uvcendim  21827  slesolex  22647  pm2mpf1  22764  mp2pm2mplem4  22774  fiinopn  22866  jensenlem2  26951  umgrupgr  29172  uspgrushgr  29246  uspgrupgr  29247  usgruspgr  29249  usgredg2vlem2  29295  cplgrop  29506  lfgrwlkprop  29754  2pthnloop  29799  usgr2pthlem  29831  elwwlks2  30037  clwlkclwwlklem2fv2  30066  eleclclwwlkn  30146  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  conngrv2edg  30265  3cyclfrgrrn1  30355  l2p  30550  strlem1  32321  ssiun2sf  32629  bnj981  35092  bnj1148  35138  swrdrevpfx  35299  consym1  36602  axc11n11  36979  bj-hbaeb2  37125  curryset  37253  currysetlem3  37256  bj-restb  37406  wl-axc11rc11  37908  clmgmOLD  38172  smgrpmgm  38185  smgrpassOLD  38186  grpomndo  38196  eldisjsim3  39258  aecom-o  39347  hbae-o  39349  hbequid  39355  equidqe  39368  equid1ALT  39371  axc11nfromc11  39372  ax12inda  39394  zindbi  43374  sdomne0  43840  exlimexi  44951  eexinst11  44954  e222  45063  e111  45101  e333  45159  stoweidlem34  46462  stoweidlem43  46471  funressnfv  47485  funbrafv  47600  ndmaovass  47648  tz6.12i-afv2  47685  dfatcolem  47697  ssfz12  47756  oexpnegnz  48148  fpprel2  48211  elclnbgrelnbgr  48295  grtriprop  48411  mgm2mgm  48697