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  1721  tbw-negdf  1722  equid  2035  nf5di  2322  hbae  2465  vtoclgaf  3543  vtoclga  3544  elinti  4917  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  vtoclr  5715  ssrelrn  5875  relresfld  6267  tz7.7  6376  elfvunirn  6901  elfvmptrab1  7008  tfisi  7843  bropopvvv  8073  f1o2ndf1  8105  xpord3inddlem  8138  suppimacnv  8158  brovex  8206  tfrlem9  8360  tfrlem11  8363  odi  8552  nndi  8597  sbth  9073  sdomdif  9101  sbthfi  9171  zorn2lem7  10474  alephexp2  10554  addcanpi  10872  mulcanpi  10873  indpi  10880  prcdnq  10966  reclem2pr  11021  lediv2a  12100  nn01to3  12956  fi1uzind  14534  cshwlen  14826  cshwidxmodr  14831  rlimres  15599  ndvdssub  16457  bitsinv1  16490  nn0seqcvgd  16618  modprm0  16855  setsstruct  17226  initoeu2  18063  symgfixelsi  19496  symgfixfo  19500  uvcendim  21957  slesolex  22800  pm2mpf1  22917  mp2pm2mplem4  22927  fiinopn  23019  jensenlem2  27110  umgrupgr  29362  uspgrushgr  29436  uspgrupgr  29437  usgruspgr  29439  usgredg2vlem2  29485  cplgrop  29696  lfgrwlkprop  29944  2pthnloop  29989  usgr2pthlem  30021  elwwlks2  30227  clwlkclwwlklem2fv2  30256  eleclclwwlkn  30336  hashecclwwlkn1  30337  umgrhashecclwwlk  30338  conngrv2edg  30455  3cyclfrgrrn1  30545  l2p  30740  strlem1  32511  ssiun2sf  32814  bnj981  35255  bnj1148  35301  swrdrevpfx  35479  consym1  36793  axc11n11  37169  bj-hbaeb2  37315  curryset  37443  currysetlem3  37446  bj-restb  37596  wl-axc11rc11  38098  clmgmOLD  38362  smgrpmgm  38375  smgrpassOLD  38376  grpomndo  38386  eldisjsim3  39448  aecom-o  39537  hbae-o  39539  hbequid  39545  equidqe  39558  equid1ALT  39561  axc11nfromc11  39562  ax12inda  39584  zindbi  43535  sdomne0  44001  exlimexi  45098  eexinst11  45101  e222  45210  e111  45248  e333  45306  stoweidlem34  46606  stoweidlem43  46615  funressnfv  47635  funbrafv  47750  ndmaovass  47798  tz6.12i-afv2  47835  dfatcolem  47847  ssfz12  47906  oexpnegnz  48298  fpprel2  48361  elclnbgrelnbgr  48445  grtriprop  48561  mgm2mgm  48847