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  566  tbw-bijust  1702  tbw-negdf  1703  equid  2016  nf5di  2285  hbae  2431  vtoclgaf  3502  vtoclga  3503  vtocl2gaf  3505  vtocl3gaf  3506  vtocl3ga  3507  vtocl4ga  3510  elinti  4885  copsexgw  5398  copsexg  5399  vtoclr  5641  ssrelrn  5792  relresfld  6168  tz7.7  6277  elfvmptrab1  6884  tfisi  7680  bropopvvv  7901  f1o2ndf1  7934  suppimacnv  7961  brovex  8009  tfrlem9  8187  tfrlem11  8190  odi  8372  nndi  8416  sbth  8833  sdomdif  8861  sbthfi  8942  zorn2lem7  10189  alephexp2  10268  addcanpi  10586  mulcanpi  10587  indpi  10594  prcdnq  10680  reclem2pr  10735  lediv2a  11799  nn01to3  12610  fi1uzind  14139  cshwlen  14440  cshwidxmodr  14445  rlimres  15195  ndvdssub  16046  bitsinv1  16077  nn0seqcvgd  16203  modprm0  16434  setsstruct  16805  initoeu2  17647  symgfixelsi  18958  symgfixfo  18962  uvcendim  20964  slesolex  21739  pm2mpf1  21856  mp2pm2mplem4  21866  fiinopn  21958  jensenlem2  26042  umgrupgr  27376  uspgrushgr  27448  uspgrupgr  27449  usgruspgr  27451  usgredg2vlem2  27496  cplgrop  27707  lfgrwlkprop  27957  2pthnloop  28000  usgr2pthlem  28032  elwwlks2  28232  clwlkclwwlklem2fv2  28261  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  conngrv2edg  28460  3cyclfrgrrn1  28550  l2p  28742  strlem1  30513  ssiun2sf  30800  bnj981  32830  bnj1148  32876  swrdrevpfx  32978  consym1  34536  axc11n11  34791  bj-hbaeb2  34928  curryset  35062  currysetlem3  35065  bj-restb  35192  wl-axc11rc11  35661  clmgmOLD  35936  smgrpmgm  35949  smgrpassOLD  35950  grpomndo  35960  aecom-o  36842  hbae-o  36844  hbequid  36850  equidqe  36863  equid1ALT  36866  axc11nfromc11  36867  ax12inda  36889  zindbi  40684  exlimexi  42033  eexinst11  42036  e222  42145  e111  42183  e333  42242  stoweidlem34  43465  stoweidlem43  43474  funressnfv  44424  funbrafv  44537  ndmaovass  44585  tz6.12i-afv2  44622  dfatcolem  44634  ssfz12  44694  oexpnegnz  45018  fpprel2  45081  mgm2mgm  45309