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  2012  nf5di  2285  hbae  2429  vtoclgaf  3542  vtoclga  3543  vtocl2gafOLD  3546  vtocl3gafOLD  3548  vtocl3gaOLD  3550  vtocl4gaOLD  3553  elinti  4919  copsexgw  5450  copsexg  5451  vtoclr  5701  ssrelrn  5858  relresfld  6249  tz7.7  6358  elfvunirn  6890  elfvmptrab1  6996  tfisi  7835  bropopvvv  8069  f1o2ndf1  8101  xpord3inddlem  8133  suppimacnv  8153  brovex  8201  tfrlem9  8353  tfrlem11  8356  odi  8543  nndi  8587  sbth  9061  sdomdif  9089  sbthfi  9163  zorn2lem7  10455  alephexp2  10534  addcanpi  10852  mulcanpi  10853  indpi  10860  prcdnq  10946  reclem2pr  11001  lediv2a  12077  nn01to3  12900  fi1uzind  14472  cshwlen  14764  cshwidxmodr  14769  rlimres  15524  ndvdssub  16379  bitsinv1  16412  nn0seqcvgd  16540  modprm0  16776  setsstruct  17146  initoeu2  17978  symgfixelsi  19365  symgfixfo  19369  uvcendim  21756  slesolex  22569  pm2mpf1  22686  mp2pm2mplem4  22696  fiinopn  22788  jensenlem2  26898  umgrupgr  29030  uspgrushgr  29104  uspgrupgr  29105  usgruspgr  29107  usgredg2vlem2  29153  cplgrop  29364  lfgrwlkprop  29615  2pthnloop  29661  usgr2pthlem  29693  elwwlks2  29896  clwlkclwwlklem2fv2  29925  eleclclwwlkn  30005  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  conngrv2edg  30124  3cyclfrgrrn1  30214  l2p  30408  strlem1  32179  ssiun2sf  32488  bnj981  34940  bnj1148  34986  swrdrevpfx  35104  consym1  36408  axc11n11  36670  bj-hbaeb2  36806  curryset  36934  currysetlem3  36937  bj-restb  37082  wl-axc11rc11  37571  clmgmOLD  37845  smgrpmgm  37858  smgrpassOLD  37859  grpomndo  37869  aecom-o  38894  hbae-o  38896  hbequid  38902  equidqe  38915  equid1ALT  38918  axc11nfromc11  38919  ax12inda  38941  zindbi  42935  sdomne0  43402  exlimexi  44514  eexinst11  44517  e222  44626  e111  44664  e333  44722  stoweidlem34  46032  stoweidlem43  46041  funressnfv  47044  funbrafv  47159  ndmaovass  47207  tz6.12i-afv2  47244  dfatcolem  47256  ssfz12  47315  oexpnegnz  47679  fpprel2  47742  elclnbgrelnbgr  47826  grtriprop  47940  mgm2mgm  48215