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  1696  tbw-negdf  1697  equid  2011  nf5di  2289  hbae  2439  vtoclgaf  3588  vtoclga  3589  vtocl2gafOLD  3592  vtocl3gafOLD  3594  vtocl3gaOLD  3596  vtocl4gaOLD  3600  elinti  4979  copsexgw  5510  copsexg  5511  vtoclr  5763  ssrelrn  5919  relresfld  6307  tz7.7  6421  elfvunirn  6952  elfvmptrab1  7057  tfisi  7896  bropopvvv  8131  f1o2ndf1  8163  xpord3inddlem  8195  suppimacnv  8215  brovex  8263  tfrlem9  8441  tfrlem11  8444  odi  8635  nndi  8679  sbth  9159  sdomdif  9191  sbthfi  9265  zorn2lem7  10571  alephexp2  10650  addcanpi  10968  mulcanpi  10969  indpi  10976  prcdnq  11062  reclem2pr  11117  lediv2a  12189  nn01to3  13006  fi1uzind  14556  cshwlen  14847  cshwidxmodr  14852  rlimres  15604  ndvdssub  16457  bitsinv1  16488  nn0seqcvgd  16617  modprm0  16852  setsstruct  17223  initoeu2  18083  symgfixelsi  19477  symgfixfo  19481  uvcendim  21890  slesolex  22709  pm2mpf1  22826  mp2pm2mplem4  22836  fiinopn  22928  jensenlem2  27049  umgrupgr  29138  uspgrushgr  29212  uspgrupgr  29213  usgruspgr  29215  usgredg2vlem2  29261  cplgrop  29472  lfgrwlkprop  29723  2pthnloop  29767  usgr2pthlem  29799  elwwlks2  29999  clwlkclwwlklem2fv2  30028  eleclclwwlkn  30108  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  conngrv2edg  30227  3cyclfrgrrn1  30317  l2p  30511  strlem1  32282  ssiun2sf  32582  bnj981  34926  bnj1148  34972  swrdrevpfx  35084  consym1  36386  axc11n11  36648  bj-hbaeb2  36784  curryset  36912  currysetlem3  36915  bj-restb  37060  wl-axc11rc11  37537  clmgmOLD  37811  smgrpmgm  37824  smgrpassOLD  37825  grpomndo  37835  aecom-o  38857  hbae-o  38859  hbequid  38865  equidqe  38878  equid1ALT  38881  axc11nfromc11  38882  ax12inda  38904  zindbi  42903  sdomne0  43375  exlimexi  44495  eexinst11  44498  e222  44607  e111  44645  e333  44704  stoweidlem34  45955  stoweidlem43  45964  funressnfv  46958  funbrafv  47073  ndmaovass  47121  tz6.12i-afv2  47158  dfatcolem  47170  ssfz12  47229  oexpnegnz  47552  fpprel2  47615  grtriprop  47792  mgm2mgm  47950