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  1699  tbw-negdf  1700  equid  2013  nf5di  2286  hbae  2430  vtoclgaf  3529  vtoclga  3530  vtocl2gafOLD  3533  vtocl3gafOLD  3535  vtocl3gaOLD  3537  vtocl4gaOLD  3540  elinti  4904  copsexgw  5428  copsexg  5429  vtoclr  5677  ssrelrn  5832  relresfld  6219  tz7.7  6328  elfvunirn  6847  elfvmptrab1  6952  tfisi  7784  bropopvvv  8015  f1o2ndf1  8047  xpord3inddlem  8079  suppimacnv  8099  brovex  8147  tfrlem9  8299  tfrlem11  8302  odi  8489  nndi  8533  sbth  9005  sdomdif  9033  sbthfi  9103  zorn2lem7  10385  alephexp2  10464  addcanpi  10782  mulcanpi  10783  indpi  10790  prcdnq  10876  reclem2pr  10931  lediv2a  12008  nn01to3  12831  fi1uzind  14406  cshwlen  14698  cshwidxmodr  14703  rlimres  15457  ndvdssub  16312  bitsinv1  16345  nn0seqcvgd  16473  modprm0  16709  setsstruct  17079  initoeu2  17915  symgfixelsi  19340  symgfixfo  19344  uvcendim  21777  slesolex  22590  pm2mpf1  22707  mp2pm2mplem4  22717  fiinopn  22809  jensenlem2  26918  umgrupgr  29074  uspgrushgr  29148  uspgrupgr  29149  usgruspgr  29151  usgredg2vlem2  29197  cplgrop  29408  lfgrwlkprop  29657  2pthnloop  29702  usgr2pthlem  29734  elwwlks2  29937  clwlkclwwlklem2fv2  29966  eleclclwwlkn  30046  hashecclwwlkn1  30047  umgrhashecclwwlk  30048  conngrv2edg  30165  3cyclfrgrrn1  30255  l2p  30449  strlem1  32220  ssiun2sf  32529  bnj981  34952  bnj1148  34998  swrdrevpfx  35129  consym1  36433  axc11n11  36695  bj-hbaeb2  36831  curryset  36959  currysetlem3  36962  bj-restb  37107  wl-axc11rc11  37596  clmgmOLD  37870  smgrpmgm  37883  smgrpassOLD  37884  grpomndo  37894  aecom-o  38919  hbae-o  38921  hbequid  38927  equidqe  38940  equid1ALT  38943  axc11nfromc11  38944  ax12inda  38966  zindbi  42958  sdomne0  43425  exlimexi  44536  eexinst11  44539  e222  44648  e111  44686  e333  44744  stoweidlem34  46051  stoweidlem43  46060  funressnfv  47053  funbrafv  47168  ndmaovass  47216  tz6.12i-afv2  47253  dfatcolem  47265  ssfz12  47324  oexpnegnz  47688  fpprel2  47751  elclnbgrelnbgr  47835  grtriprop  47951  mgm2mgm  48237