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  211  anidms  567  tbw-bijust  1701  tbw-negdf  1702  equid  2016  nf5di  2283  hbae  2432  vtoclgaf  3513  vtoclga  3514  vtocl2gaf  3516  vtocl3gaf  3517  vtocl3ga  3518  vtocl4ga  3521  elinti  4889  copsexgw  5405  copsexg  5406  vtoclr  5651  ssrelrn  5806  relresfld  6183  tz7.7  6296  elfvmptrab1  6911  tfisi  7714  bropopvvv  7939  f1o2ndf1  7972  suppimacnv  7999  brovex  8047  tfrlem9  8225  tfrlem11  8228  odi  8419  nndi  8463  sbth  8889  sdomdif  8921  sbthfi  8994  zorn2lem7  10267  alephexp2  10346  addcanpi  10664  mulcanpi  10665  indpi  10672  prcdnq  10758  reclem2pr  10813  lediv2a  11878  nn01to3  12690  fi1uzind  14220  cshwlen  14521  cshwidxmodr  14526  rlimres  15276  ndvdssub  16127  bitsinv1  16158  nn0seqcvgd  16284  modprm0  16515  setsstruct  16886  initoeu2  17740  symgfixelsi  19052  symgfixfo  19056  uvcendim  21063  slesolex  21840  pm2mpf1  21957  mp2pm2mplem4  21967  fiinopn  22059  jensenlem2  26146  umgrupgr  27482  uspgrushgr  27554  uspgrupgr  27555  usgruspgr  27557  usgredg2vlem2  27602  cplgrop  27813  lfgrwlkprop  28064  2pthnloop  28108  usgr2pthlem  28140  elwwlks2  28340  clwlkclwwlklem2fv2  28369  eleclclwwlkn  28449  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  conngrv2edg  28568  3cyclfrgrrn1  28658  l2p  28850  strlem1  30621  ssiun2sf  30908  bnj981  32939  bnj1148  32985  swrdrevpfx  33087  consym1  34618  axc11n11  34873  bj-hbaeb2  35010  curryset  35144  currysetlem3  35147  bj-restb  35274  wl-axc11rc11  35743  clmgmOLD  36018  smgrpmgm  36031  smgrpassOLD  36032  grpomndo  36042  aecom-o  36922  hbae-o  36924  hbequid  36930  equidqe  36943  equid1ALT  36946  axc11nfromc11  36947  ax12inda  36969  zindbi  40775  exlimexi  42151  eexinst11  42154  e222  42263  e111  42301  e333  42360  stoweidlem34  43582  stoweidlem43  43591  funressnfv  44548  funbrafv  44661  ndmaovass  44709  tz6.12i-afv2  44746  dfatcolem  44758  ssfz12  44817  oexpnegnz  45141  fpprel2  45204  mgm2mgm  45432