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  214  anidms  573  tbw-bijust  1712  tbw-negdf  1713  equid  2026  nf5di  2313  hbae  2456  vtoclgaf  3535  vtoclga  3536  elinti  4908  copsexgw  5452  copsexgwOLD  5453  copsexg  5454  vtoclr  5703  ssrelrn  5863  relresfld  6252  tz7.7  6361  elfvunirn  6886  elfvmptrab1  6993  tfisi  7828  bropopvvv  8057  f1o2ndf1  8089  xpord3inddlem  8122  suppimacnv  8142  brovex  8190  tfrlem9  8344  tfrlem11  8347  odi  8536  nndi  8581  sbth  9058  sdomdif  9086  sbthfi  9156  zorn2lem7  10449  alephexp2  10529  addcanpi  10847  mulcanpi  10848  indpi  10855  prcdnq  10941  reclem2pr  10996  lediv2a  12076  nn01to3  12932  fi1uzind  14510  cshwlen  14802  cshwidxmodr  14807  rlimres  15561  ndvdssub  16419  bitsinv1  16452  nn0seqcvgd  16580  modprm0  16817  setsstruct  17188  initoeu2  18025  symgfixelsi  19451  symgfixfo  19455  uvcendim  21872  slesolex  22715  pm2mpf1  22832  mp2pm2mplem4  22842  fiinopn  22934  jensenlem2  27022  umgrupgr  29243  uspgrushgr  29317  uspgrupgr  29318  usgruspgr  29320  usgredg2vlem2  29366  cplgrop  29577  lfgrwlkprop  29825  2pthnloop  29870  usgr2pthlem  29902  elwwlks2  30108  clwlkclwwlklem2fv2  30137  eleclclwwlkn  30217  hashecclwwlkn1  30218  umgrhashecclwwlk  30219  conngrv2edg  30336  3cyclfrgrrn1  30426  l2p  30621  strlem1  32392  ssiun2sf  32701  bnj981  35202  bnj1148  35248  swrdrevpfx  35415  consym1  36728  axc11n11  37105  bj-hbaeb2  37251  curryset  37379  currysetlem3  37382  bj-restb  37532  wl-axc11rc11  38034  clmgmOLD  38298  smgrpmgm  38311  smgrpassOLD  38312  grpomndo  38322  eldisjsim3  39384  aecom-o  39473  hbae-o  39475  hbequid  39481  equidqe  39494  equid1ALT  39497  axc11nfromc11  39498  ax12inda  39520  zindbi  43471  sdomne0  43937  exlimexi  45048  eexinst11  45051  e222  45160  e111  45198  e333  45256  stoweidlem34  46556  stoweidlem43  46565  funressnfv  47585  funbrafv  47700  ndmaovass  47748  tz6.12i-afv2  47785  dfatcolem  47797  ssfz12  47856  oexpnegnz  48248  fpprel2  48311  elclnbgrelnbgr  48395  grtriprop  48511  mgm2mgm  48797