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  1700  tbw-negdf  1701  equid  2014  nf5di  2292  hbae  2436  vtoclgaf  3532  vtoclga  3533  vtocl2gafOLD  3536  vtocl3gafOLD  3538  vtocl3gaOLD  3540  vtocl4gaOLD  3543  elinti  4912  copsexgw  5439  copsexg  5440  vtoclr  5688  ssrelrn  5844  relresfld  6235  tz7.7  6344  elfvunirn  6865  elfvmptrab1  6971  tfisi  7803  bropopvvv  8034  f1o2ndf1  8066  xpord3inddlem  8098  suppimacnv  8118  brovex  8166  tfrlem9  8318  tfrlem11  8321  odi  8508  nndi  8553  sbth  9029  sdomdif  9057  sbthfi  9127  zorn2lem7  10416  alephexp2  10496  addcanpi  10814  mulcanpi  10815  indpi  10822  prcdnq  10908  reclem2pr  10963  lediv2a  12040  nn01to3  12858  fi1uzind  14434  cshwlen  14726  cshwidxmodr  14731  rlimres  15485  ndvdssub  16340  bitsinv1  16373  nn0seqcvgd  16501  modprm0  16737  setsstruct  17107  initoeu2  17944  symgfixelsi  19368  symgfixfo  19372  uvcendim  21806  slesolex  22630  pm2mpf1  22747  mp2pm2mplem4  22757  fiinopn  22849  jensenlem2  26958  umgrupgr  29159  uspgrushgr  29233  uspgrupgr  29234  usgruspgr  29236  usgredg2vlem2  29282  cplgrop  29493  lfgrwlkprop  29742  2pthnloop  29787  usgr2pthlem  29819  elwwlks2  30025  clwlkclwwlklem2fv2  30054  eleclclwwlkn  30134  hashecclwwlkn1  30135  umgrhashecclwwlk  30136  conngrv2edg  30253  3cyclfrgrrn1  30343  l2p  30537  strlem1  32308  ssiun2sf  32616  bnj981  35087  bnj1148  35133  swrdrevpfx  35292  consym1  36595  axc11n11  36858  bj-hbaeb2  36994  curryset  37122  currysetlem3  37125  bj-restb  37270  wl-axc11rc11  37759  clmgmOLD  38023  smgrpmgm  38036  smgrpassOLD  38037  grpomndo  38047  eldisjsim3  39109  aecom-o  39198  hbae-o  39200  hbequid  39206  equidqe  39219  equid1ALT  39222  axc11nfromc11  39223  ax12inda  39245  zindbi  43224  sdomne0  43690  exlimexi  44801  eexinst11  44804  e222  44913  e111  44951  e333  45009  stoweidlem34  46314  stoweidlem43  46323  funressnfv  47325  funbrafv  47440  ndmaovass  47488  tz6.12i-afv2  47525  dfatcolem  47537  ssfz12  47596  oexpnegnz  47960  fpprel2  48023  elclnbgrelnbgr  48107  grtriprop  48223  mgm2mgm  48509