Theorem pm2.43i 50

Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 54. (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  63  pm2.18  121  impbid  201  ibi  255  anidms  675  3imp3i2an  1270  tbw-bijust  1614  tbw-negdf  1615  equid  1926  nf5di  2105  nfdiOLD  2213  hbae  2303  vtoclgaf  3244  vtocl2gaf  3246  vtocl3gaf  3248  vtocl4ga  3251  elinti  4420  copsexg  4882  vtoclr  5086  ssrelrn  5237  issref  5428  relresfld  5579  tz7.7  5666  elfvmptrab1  6213  tfisi  6950  bropopvvv  7142  f1o2ndf1  7172  suppimacnv  7193  brovex  7235  tfrlem9  7368  tfrlem11  7371  odi  7546  nndi  7590  sbth  7965  sdomdif  7993  zorn2lem7  9207  alephexp2  9282  addcanpi  9600  mulcanpi  9601  indpi  9608  prcdnq  9694  reclem2pr  9749  lediv2a  10796  nn01to3  11657  fi1uzind  13134  fi1uzindOLD  13140  cshwlen  13396  cshwidxmodr  13401  rlimres  14137  ndvdssub  14971  bitsinv1  15002  nn0seqcvgd  15121  modprm0  15348  initoeu2  16489  symgfixelsi  17678  symgfixfo  17682  uvcendim  20005  slesolex  20307  pm2mpf1  20423  mp2pm2mplem4  20433  fiinopn  20531  jensenlem2  24514  umgrupgr  25769  usgraidx2vlem2  25921  wlkcompim  26054  wlkdvspthlem  26137  usgra2adedgspthlem2  26140  clwlkcompim  26292  clwwlknprop  26300  clwlkisclwwlklem2fv2  26311  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlkfclwwlk  26371  el2wlkonot  26396  2wlkonot3v  26402  2spthonot3v  26403  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  extwwlkfablem2  26605  numclwlk1lem2foa  26618  frgrareg  26644  strlem1  28493  vtocl2d  28699  ssiun2sf  28760  bnj981  30274  bnj1148  30318  consym1  31589  axc11n11  31859  bj-hbaeb2  31993  bj-restb  32228  clmgmOLD  32820  smgrpmgm  32833  smgrpassOLD  32834  grpomndo  32844  aecom-o  33204  hbae-o  33206  hbequid  33212  equidqe  33225  equid1ALT  33228  axc11nfromc11  33229  ax12inda  33251  zindbi  36529  exlimexi  37751  eexinst11  37754  e222  37882  e111  37920  e333  37981  stoweidlem34  38927  stoweidlem43  38936  funressnfv  39857  funbrafv  39887  ndmaovass  39935  oexpnegALTV  40126  oexpnegnz  40127  ssfz12  40351  uspgrushgr  40405  uspgrupgr  40406  usgruspgr  40408  usgredg2vlem2  40453  cplgrop  40659  lfgrwlkprop  40896  2pthnloop  40937  usgr2pthlem  40969  uspgrn2crct  41011  elwwlks2  41170  clwlkclwwlklem2fv2  41205  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfclwwlk  41269  conngrv2edg  41362  frgrusgrfrcond  41431  3cyclfrgrrn1  41455  av-numclwlk1lem2foa  41521  mgm2mgm  41653