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  1699  tbw-negdf  1700  equid  2014  nf5di  2280  hbae  2429  vtoclgaf  3565  vtoclga  3566  vtocl2gaf  3568  vtocl3gaf  3569  vtocl3ga  3570  vtocl4ga  3573  elinti  4959  copsexgw  5490  copsexg  5491  vtoclr  5739  ssrelrn  5894  relresfld  6275  tz7.7  6390  elfvunirn  6923  elfvmptrab1  7025  tfisi  7852  bropopvvv  8081  f1o2ndf1  8113  xpord3inddlem  8145  suppimacnv  8164  brovex  8213  tfrlem9  8391  tfrlem11  8394  odi  8585  nndi  8629  sbth  9099  sdomdif  9131  sbthfi  9208  zorn2lem7  10503  alephexp2  10582  addcanpi  10900  mulcanpi  10901  indpi  10908  prcdnq  10994  reclem2pr  11049  lediv2a  12115  nn01to3  12932  fi1uzind  14465  cshwlen  14756  cshwidxmodr  14761  rlimres  15509  ndvdssub  16359  bitsinv1  16390  nn0seqcvgd  16514  modprm0  16745  setsstruct  17116  initoeu2  17976  symgfixelsi  19351  symgfixfo  19355  uvcendim  21713  slesolex  22505  pm2mpf1  22622  mp2pm2mplem4  22632  fiinopn  22724  jensenlem2  26835  umgrupgr  28798  uspgrushgr  28870  uspgrupgr  28871  usgruspgr  28873  usgredg2vlem2  28918  cplgrop  29129  lfgrwlkprop  29379  2pthnloop  29423  usgr2pthlem  29455  elwwlks2  29655  clwlkclwwlklem2fv2  29684  eleclclwwlkn  29764  hashecclwwlkn1  29765  umgrhashecclwwlk  29766  conngrv2edg  29883  3cyclfrgrrn1  29973  l2p  30167  strlem1  31938  ssiun2sf  32226  bnj981  34427  bnj1148  34473  swrdrevpfx  34573  consym1  35772  axc11n11  36027  bj-hbaeb2  36163  curryset  36294  currysetlem3  36297  bj-restb  36442  wl-axc11rc11  36912  clmgmOLD  37186  smgrpmgm  37199  smgrpassOLD  37200  grpomndo  37210  aecom-o  38238  hbae-o  38240  hbequid  38246  equidqe  38259  equid1ALT  38262  axc11nfromc11  38263  ax12inda  38285  zindbi  42151  sdomne0  42630  exlimexi  43751  eexinst11  43754  e222  43863  e111  43901  e333  43960  stoweidlem34  45212  stoweidlem43  45221  funressnfv  46215  funbrafv  46328  ndmaovass  46376  tz6.12i-afv2  46413  dfatcolem  46425  ssfz12  46484  oexpnegnz  46808  fpprel2  46871  mgm2mgm  47067