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  213  anidms  571  tbw-bijust  1705  tbw-negdf  1706  equid  2019  nf5di  2296  hbae  2439  vtoclgaf  3522  vtoclga  3523  vtocl2gafOLD  3526  vtocl3gafOLD  3528  vtocl3gaOLD  3530  vtocl4gaOLD  3533  elinti  4893  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  vtoclr  5688  ssrelrn  5843  relresfld  6234  tz7.7  6343  elfvunirn  6864  elfvmptrab1  6971  tfisi  7806  bropopvvv  8036  f1o2ndf1  8068  xpord3inddlem  8101  suppimacnv  8121  brovex  8169  tfrlem9  8321  tfrlem11  8324  odi  8511  nndi  8556  sbth  9032  sdomdif  9060  sbthfi  9130  zorn2lem7  10422  alephexp2  10502  addcanpi  10820  mulcanpi  10821  indpi  10828  prcdnq  10914  reclem2pr  10969  lediv2a  12048  nn01to3  12889  fi1uzind  14467  cshwlen  14759  cshwidxmodr  14764  rlimres  15518  ndvdssub  16376  bitsinv1  16409  nn0seqcvgd  16537  modprm0  16774  setsstruct  17144  initoeu2  17981  symgfixelsi  19408  symgfixfo  19412  uvcendim  21829  slesolex  22672  pm2mpf1  22789  mp2pm2mplem4  22799  fiinopn  22891  jensenlem2  26976  umgrupgr  29197  uspgrushgr  29271  uspgrupgr  29272  usgruspgr  29274  usgredg2vlem2  29320  cplgrop  29531  lfgrwlkprop  29779  2pthnloop  29824  usgr2pthlem  29856  elwwlks2  30062  clwlkclwwlklem2fv2  30091  eleclclwwlkn  30171  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  conngrv2edg  30290  3cyclfrgrrn1  30380  l2p  30575  strlem1  32346  ssiun2sf  32655  bnj981  35139  bnj1148  35185  swrdrevpfx  35346  consym1  36649  axc11n11  37026  bj-hbaeb2  37172  curryset  37300  currysetlem3  37303  bj-restb  37453  wl-axc11rc11  37955  clmgmOLD  38219  smgrpmgm  38232  smgrpassOLD  38233  grpomndo  38243  eldisjsim3  39305  aecom-o  39394  hbae-o  39396  hbequid  39402  equidqe  39415  equid1ALT  39418  axc11nfromc11  39419  ax12inda  39441  zindbi  43392  sdomne0  43858  exlimexi  44969  eexinst11  44972  e222  45081  e111  45119  e333  45177  stoweidlem34  46478  stoweidlem43  46487  funressnfv  47507  funbrafv  47622  ndmaovass  47670  tz6.12i-afv2  47707  dfatcolem  47719  ssfz12  47778  oexpnegnz  48170  fpprel2  48233  elclnbgrelnbgr  48317  grtriprop  48433  mgm2mgm  48719