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  1698  tbw-negdf  1699  equid  2011  nf5di  2285  hbae  2436  vtoclgaf  3576  vtoclga  3577  vtocl2gafOLD  3580  vtocl3gafOLD  3582  vtocl3gaOLD  3584  vtocl4gaOLD  3587  elinti  4955  copsexgw  5495  copsexg  5496  vtoclr  5748  ssrelrn  5905  relresfld  6296  tz7.7  6410  elfvunirn  6938  elfvmptrab1  7044  tfisi  7880  bropopvvv  8115  f1o2ndf1  8147  xpord3inddlem  8179  suppimacnv  8199  brovex  8247  tfrlem9  8425  tfrlem11  8428  odi  8617  nndi  8661  sbth  9133  sdomdif  9165  sbthfi  9239  zorn2lem7  10542  alephexp2  10621  addcanpi  10939  mulcanpi  10940  indpi  10947  prcdnq  11033  reclem2pr  11088  lediv2a  12162  nn01to3  12983  fi1uzind  14546  cshwlen  14837  cshwidxmodr  14842  rlimres  15594  ndvdssub  16446  bitsinv1  16479  nn0seqcvgd  16607  modprm0  16843  setsstruct  17213  initoeu2  18061  symgfixelsi  19453  symgfixfo  19457  uvcendim  21867  slesolex  22688  pm2mpf1  22805  mp2pm2mplem4  22815  fiinopn  22907  jensenlem2  27031  umgrupgr  29120  uspgrushgr  29194  uspgrupgr  29195  usgruspgr  29197  usgredg2vlem2  29243  cplgrop  29454  lfgrwlkprop  29705  2pthnloop  29751  usgr2pthlem  29783  elwwlks2  29986  clwlkclwwlklem2fv2  30015  eleclclwwlkn  30095  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  conngrv2edg  30214  3cyclfrgrrn1  30304  l2p  30498  strlem1  32269  ssiun2sf  32572  bnj981  34964  bnj1148  35010  swrdrevpfx  35122  consym1  36421  axc11n11  36683  bj-hbaeb2  36819  curryset  36947  currysetlem3  36950  bj-restb  37095  wl-axc11rc11  37584  clmgmOLD  37858  smgrpmgm  37871  smgrpassOLD  37872  grpomndo  37882  aecom-o  38902  hbae-o  38904  hbequid  38910  equidqe  38923  equid1ALT  38926  axc11nfromc11  38927  ax12inda  38949  zindbi  42958  sdomne0  43426  exlimexi  44544  eexinst11  44547  e222  44656  e111  44694  e333  44753  stoweidlem34  46049  stoweidlem43  46058  funressnfv  47055  funbrafv  47170  ndmaovass  47218  tz6.12i-afv2  47255  dfatcolem  47267  ssfz12  47326  oexpnegnz  47665  fpprel2  47728  elclnbgrelnbgr  47812  grtriprop  47908  mgm2mgm  48143