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  pm2.18  125  impbid  204  ibi  259  anidms  562  tbw-bijust  1742  tbw-negdf  1743  equid  2059  nf5di  2259  hbae  2397  vtoclgaf  3473  vtocl2gaf  3475  vtocl3gaf  3477  vtocl4ga  3480  elinti  4721  copsexg  5189  vtoclr  5414  ssrelrn  5562  idrefOLD  5766  relresfld  5918  tz7.7  6004  elfvmptrab1  6569  tfisi  7338  bropopvvv  7538  f1o2ndf1  7568  suppimacnv  7589  brovex  7632  tfrlem9  7766  tfrlem11  7769  odi  7945  nndi  7989  sbth  8370  sdomdif  8398  zorn2lem7  9661  alephexp2  9740  addcanpi  10058  mulcanpi  10059  indpi  10066  prcdnq  10152  reclem2pr  10207  lediv2a  11273  nn01to3  12092  fi1uzind  13597  cshwlen  13954  cshwidxmodr  13959  rlimres  14701  ndvdssub  15543  bitsinv1  15574  nn0seqcvgd  15693  modprm0  15918  setsstruct  16299  initoeu2  17055  symgfixelsi  18242  symgfixfo  18246  uvcendim  20594  slesolex  20898  pm2mpf1  21015  mp2pm2mplem4  21025  fiinopn  21117  jensenlem2  25170  umgrupgr  26455  uspgrushgr  26528  uspgrupgr  26529  usgruspgr  26531  usgredg2vlem2  26576  cplgrop  26789  lfgrwlkprop  27042  2pthnloop  27087  usgr2pthlem  27119  elwwlks2  27350  clwlkclwwlklem2fv2  27380  eleclclwwlkn  27478  hashecclwwlkn1  27479  umgrhashecclwwlk  27480  conngrv2edg  27602  frgrusgrfrcond  27671  3cyclfrgrrn1  27697  l2p  27910  strlem1  29685  vtocl2d  29890  ssiun2sf  29944  bnj981  31623  bnj1148  31667  consym1  33006  axc11n11  33265  bj-hbaeb2  33384  bj-restb  33624  bj-ismoored0  33638  clmgmOLD  34279  smgrpmgm  34292  smgrpassOLD  34293  grpomndo  34303  aecom-o  35060  hbae-o  35062  hbequid  35068  equidqe  35081  equid1ALT  35084  axc11nfromc11  35085  ax12inda  35107  zindbi  38480  exlimexi  39694  eexinst11  39697  e222  39815  e111  39853  e333  39912  stoweidlem34  41188  stoweidlem43  41197  funressnfv  42117  funbrafv  42209  ndmaovass  42257  tz6.12i-afv2  42294  dfatcolem  42306  ssfz12  42366  oexpnegnz  42624  mgm2mgm  42888