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  2430  vtoclgaf  3545  vtoclga  3546  vtocl2gafOLD  3549  vtocl3gafOLD  3551  vtocl3gaOLD  3553  vtocl4gaOLD  3556  elinti  4922  copsexgw  5453  copsexg  5454  vtoclr  5704  ssrelrn  5861  relresfld  6252  tz7.7  6361  elfvunirn  6893  elfvmptrab1  6999  tfisi  7838  bropopvvv  8072  f1o2ndf1  8104  xpord3inddlem  8136  suppimacnv  8156  brovex  8204  tfrlem9  8356  tfrlem11  8359  odi  8546  nndi  8590  sbth  9067  sdomdif  9095  sbthfi  9169  zorn2lem7  10462  alephexp2  10541  addcanpi  10859  mulcanpi  10860  indpi  10867  prcdnq  10953  reclem2pr  11008  lediv2a  12084  nn01to3  12907  fi1uzind  14479  cshwlen  14771  cshwidxmodr  14776  rlimres  15531  ndvdssub  16386  bitsinv1  16419  nn0seqcvgd  16547  modprm0  16783  setsstruct  17153  initoeu2  17985  symgfixelsi  19372  symgfixfo  19376  uvcendim  21763  slesolex  22576  pm2mpf1  22693  mp2pm2mplem4  22703  fiinopn  22795  jensenlem2  26905  umgrupgr  29037  uspgrushgr  29111  uspgrupgr  29112  usgruspgr  29114  usgredg2vlem2  29160  cplgrop  29371  lfgrwlkprop  29622  2pthnloop  29668  usgr2pthlem  29700  elwwlks2  29903  clwlkclwwlklem2fv2  29932  eleclclwwlkn  30012  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  conngrv2edg  30131  3cyclfrgrrn1  30221  l2p  30415  strlem1  32186  ssiun2sf  32495  bnj981  34947  bnj1148  34993  swrdrevpfx  35111  consym1  36415  axc11n11  36677  bj-hbaeb2  36813  curryset  36941  currysetlem3  36944  bj-restb  37089  wl-axc11rc11  37578  clmgmOLD  37852  smgrpmgm  37865  smgrpassOLD  37866  grpomndo  37876  aecom-o  38901  hbae-o  38903  hbequid  38909  equidqe  38922  equid1ALT  38925  axc11nfromc11  38926  ax12inda  38948  zindbi  42942  sdomne0  43409  exlimexi  44521  eexinst11  44524  e222  44633  e111  44671  e333  44729  stoweidlem34  46039  stoweidlem43  46048  funressnfv  47048  funbrafv  47163  ndmaovass  47211  tz6.12i-afv2  47248  dfatcolem  47260  ssfz12  47319  oexpnegnz  47683  fpprel2  47746  elclnbgrelnbgr  47830  grtriprop  47944  mgm2mgm  48219