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  1694  tbw-negdf  1695  equid  2008  nf5di  2283  hbae  2433  vtoclgaf  3575  vtoclga  3576  vtocl2gafOLD  3579  vtocl3gafOLD  3581  vtocl3gaOLD  3583  vtocl4gaOLD  3586  elinti  4959  copsexgw  5500  copsexg  5501  vtoclr  5751  ssrelrn  5907  relresfld  6297  tz7.7  6411  elfvunirn  6938  elfvmptrab1  7043  tfisi  7879  bropopvvv  8113  f1o2ndf1  8145  xpord3inddlem  8177  suppimacnv  8197  brovex  8245  tfrlem9  8423  tfrlem11  8426  odi  8615  nndi  8659  sbth  9131  sdomdif  9163  sbthfi  9236  zorn2lem7  10539  alephexp2  10618  addcanpi  10936  mulcanpi  10937  indpi  10944  prcdnq  11030  reclem2pr  11085  lediv2a  12159  nn01to3  12980  fi1uzind  14542  cshwlen  14833  cshwidxmodr  14838  rlimres  15590  ndvdssub  16442  bitsinv1  16475  nn0seqcvgd  16603  modprm0  16838  setsstruct  17209  initoeu2  18069  symgfixelsi  19467  symgfixfo  19471  uvcendim  21884  slesolex  22703  pm2mpf1  22820  mp2pm2mplem4  22830  fiinopn  22922  jensenlem2  27045  umgrupgr  29134  uspgrushgr  29208  uspgrupgr  29209  usgruspgr  29211  usgredg2vlem2  29257  cplgrop  29468  lfgrwlkprop  29719  2pthnloop  29763  usgr2pthlem  29795  elwwlks2  29995  clwlkclwwlklem2fv2  30024  eleclclwwlkn  30104  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  conngrv2edg  30223  3cyclfrgrrn1  30313  l2p  30507  strlem1  32278  ssiun2sf  32579  bnj981  34942  bnj1148  34988  swrdrevpfx  35100  consym1  36402  axc11n11  36664  bj-hbaeb2  36800  curryset  36928  currysetlem3  36931  bj-restb  37076  wl-axc11rc11  37563  clmgmOLD  37837  smgrpmgm  37850  smgrpassOLD  37851  grpomndo  37861  aecom-o  38882  hbae-o  38884  hbequid  38890  equidqe  38903  equid1ALT  38906  axc11nfromc11  38907  ax12inda  38929  zindbi  42934  sdomne0  43402  exlimexi  44521  eexinst11  44524  e222  44633  e111  44671  e333  44730  stoweidlem34  45989  stoweidlem43  45998  funressnfv  46992  funbrafv  47107  ndmaovass  47155  tz6.12i-afv2  47192  dfatcolem  47204  ssfz12  47263  oexpnegnz  47602  fpprel2  47665  elclnbgrelnbgr  47749  grtriprop  47845  mgm2mgm  48070