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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  sylc  66  impbid  215  anidms  577  tbw-bijust  1730  tbw-negdf  1731  equid  2044  nf5di  2318  hbae  2460  vtoclgaf  3535  vtoclga  3536  elinti  4915  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  cotsexgw  5462  vtoclr  5713  ssrelrn  5875  relresfldOLD  6279  tz7.7  6388  elfvunirn  6915  elfvmptrab1  7022  tfisi  7870  bropopvvv  8101  f1o2ndf1  8133  xpord3inddlem  8171  suppimacnv  8192  brovex  8240  tfrlem9  8394  tfrlem11  8397  odi  8588  nndi  8633  sbth  9117  sdomdif  9145  sbthfi  9215  zorn2lem7  10581  alephexp2  10667  addcanpi  10985  mulcanpi  10986  indpi  10993  prcdnq  11079  reclem2pr  11134  lediv2a  12212  nn01to3  13069  fi1uzind  14653  swrdrevpfx  14919  cshwlen  14951  cshwidxmodr  14956  rlimres  15726  ndvdssub  16580  bitsinv1  16613  nn0seqcvgd  16746  modprm0  16984  setsstruct  17355  initoeu2  18192  symgfixelsi  19650  symgfixfo  19654  uvcendim  22154  slesolex  23001  pm2mpf1  23118  mp2pm2mplem4  23128  fiinopn  23220  jensenlem2  27316  umgrupgr  29682  uspgrushgr  29759  uspgrupgr  29760  usgruspgr  29762  usgredg2vlem2  29808  cplgrop  30019  lfgrwlkprop  30271  2pthnloop  30318  usgr2pthlem  30350  elwwlks2  30559  clwlkclwwlklem2fv2  30588  eleclclwwlkn  30668  hashecclwwlkn1  30669  umgrhashecclwwlk  30670  conngrv2edg  30797  3cyclfrgrrn1  30887  l2p  31082  strlem1  32853  ssiun2sf  33197  bnj981  35623  bnj1148  35669  dfac16  35803  weexenwe  35805  kardfi  35887  consym1  37283  axc11n11  37659  bj-hbaeb2  37805  curryset  37934  currysetlem3  37937  bj-restb  38090  wl-axc11rc11  38591  clmgmOLD  38861  smgrpmgm  38874  smgrpassOLD  38875  grpomndo  38885  eldisjsim3  39945  aecom-o  40034  hbae-o  40036  hbequid  40042  equidqe  40055  equid1ALT  40058  axc11nfromc11  40059  ax12inda  40081  zindbi  44029  sdomne0  44490  exlimexi  45583  eexinst11  45586  e222  45695  e111  45733  e333  45791  stoweidlem34  47120  stoweidlem43  47129  funressnfv  48189  funbrafv  48304  ndmaovass  48352  tz6.12i-afv2  48389  dfatcolem  48401  ssfz12  48460  oexpnegnz  48852  fpprel2  48915  elclnbgrelnbgr  48999  grtriprop  49115  mgm2mgm  49400