Theorem pm2.43i 53

Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 57. (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 23	. 2 ⊢ (𝜑 → 𝜑)
2		pm2.43i.1	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	1, 2	mpd 16	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  sylc  66  impbid  215  anidms  577  tbw-bijust  1731  tbw-negdf  1732  equid  2047  nf5di  2184  nf5diOLD  2322  hbae  2463  vtoclgaf  3539  vtoclga  3540  elinti  4919  copsexgw  5464  copsexgwOLD  5465  copsexg  5466  cotsexgw  5467  vtoclr  5718  ssrelrn  5883  relresfldOLD  6297  tz7.7  6406  elfvunirn  6938  elfvmptrab1  7045  tfisi  7894  bropopvvv  8126  f1o2ndf1  8160  xpord3inddlem  8198  suppimacnv  8219  brovex  8267  tfrlem9  8421  tfrlem11  8424  odi  8615  nndi  8660  sbth  9144  sdomdif  9172  sbthfi  9242  zorn2lem7  10607  alephexp2  10693  addcanpi  11011  mulcanpi  11012  indpi  11019  prcdnq  11105  reclem2pr  11160  lediv2a  12238  nn01to3  13095  fi1uzind  14679  swrdrevpfx  14946  cshwlen  14978  cshwidxmodr  14983  rlimres  15754  ndvdssub  16608  bitsinv1  16641  nn0seqcvgd  16774  modprm0  17012  setsstruct  17383  initoeu2  18220  symgfixelsi  19679  symgfixfo  19683  uvcendim  22183  slesolex  23030  pm2mpf1  23147  mp2pm2mplem4  23157  fiinopn  23249  jensenlem2  27345  umgrupgr  29711  uspgrushgr  29788  uspgrupgr  29789  usgruspgr  29791  usgredg2vlem2  29837  cplgrop  30048  lfgrwlkprop  30300  2pthnloop  30347  usgr2pthlem  30379  elwwlks2  30588  clwlkclwwlklem2fv2  30617  eleclclwwlkn  30697  hashecclwwlkn1  30698  umgrhashecclwwlk  30699  conngrv2edg  30826  3cyclfrgrrn1  30916  l2p  31111  strlem1  32882  ssiun2sf  33226  bnj981  35650  bnj1148  35696  dfac16  35846  weexenwe  35848  kardfi  35938  consym1  37386  axc11n11  37762  bj-hbaeb2  37908  curryset  38037  currysetlem3  38040  bj-restb  38206  wl-axc11rc11  38707  clmgmOLD  38977  smgrpmgm  38990  smgrpassOLD  38991  grpomndo  39001  eldisjsim3  40061  aecom-o  40150  hbae-o  40152  hbequid  40158  equidqe  40171  equid1ALT  40174  axc11nfromc11  40175  ax12inda  40197  zindbi  44146  sdomne0  44606  exlimexi  45698  eexinst11  45701  e222  45810  e111  45848  e333  45906  stoweidlem34  47249  stoweidlem43  47258  funressnfv  48318  funbrafv  48433  ndmaovass  48481  tz6.12i-afv2  48518  dfatcolem  48530  ssfz12  48589  oexpnegnz  48981  fpprel2  49044  elclnbgrelnbgr  49128  grtriprop  49244  mgm2mgm  49529