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  1700  tbw-negdf  1701  equid  2014  nf5di  2292  hbae  2436  vtoclgaf  3520  vtoclga  3521  vtocl2gafOLD  3524  vtocl3gafOLD  3526  vtocl3gaOLD  3528  vtocl4gaOLD  3531  elinti  4899  copsexgw  5436  copsexg  5437  vtoclr  5685  ssrelrn  5841  relresfld  6232  tz7.7  6341  elfvunirn  6862  elfvmptrab1  6968  tfisi  7801  bropopvvv  8031  f1o2ndf1  8063  xpord3inddlem  8095  suppimacnv  8115  brovex  8163  tfrlem9  8315  tfrlem11  8318  odi  8505  nndi  8550  sbth  9026  sdomdif  9054  sbthfi  9124  zorn2lem7  10413  alephexp2  10493  addcanpi  10811  mulcanpi  10812  indpi  10819  prcdnq  10905  reclem2pr  10960  lediv2a  12039  nn01to3  12880  fi1uzind  14458  cshwlen  14750  cshwidxmodr  14755  rlimres  15509  ndvdssub  16367  bitsinv1  16400  nn0seqcvgd  16528  modprm0  16765  setsstruct  17135  initoeu2  17972  symgfixelsi  19399  symgfixfo  19403  uvcendim  21835  slesolex  22656  pm2mpf1  22773  mp2pm2mplem4  22783  fiinopn  22875  jensenlem2  26969  umgrupgr  29191  uspgrushgr  29265  uspgrupgr  29266  usgruspgr  29268  usgredg2vlem2  29314  cplgrop  29525  lfgrwlkprop  29774  2pthnloop  29819  usgr2pthlem  29851  elwwlks2  30057  clwlkclwwlklem2fv2  30086  eleclclwwlkn  30166  hashecclwwlkn1  30167  umgrhashecclwwlk  30168  conngrv2edg  30285  3cyclfrgrrn1  30375  l2p  30570  strlem1  32341  ssiun2sf  32649  bnj981  35113  bnj1148  35159  swrdrevpfx  35320  consym1  36623  axc11n11  36992  bj-hbaeb2  37138  curryset  37266  currysetlem3  37269  bj-restb  37419  wl-axc11rc11  37919  clmgmOLD  38183  smgrpmgm  38196  smgrpassOLD  38197  grpomndo  38207  eldisjsim3  39269  aecom-o  39358  hbae-o  39360  hbequid  39366  equidqe  39379  equid1ALT  39382  axc11nfromc11  39383  ax12inda  39405  zindbi  43389  sdomne0  43855  exlimexi  44966  eexinst11  44969  e222  45078  e111  45116  e333  45174  stoweidlem34  46477  stoweidlem43  46486  funressnfv  47488  funbrafv  47603  ndmaovass  47651  tz6.12i-afv2  47688  dfatcolem  47700  ssfz12  47759  oexpnegnz  48151  fpprel2  48214  elclnbgrelnbgr  48298  grtriprop  48414  mgm2mgm  48700