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  3533  vtoclga  3534  vtocl2gafOLD  3537  vtocl3gafOLD  3539  vtocl3gaOLD  3541  vtocl4gaOLD  3544  elinti  4913  copsexgw  5446  copsexg  5447  vtoclr  5695  ssrelrn  5851  relresfld  6242  tz7.7  6351  elfvunirn  6872  elfvmptrab1  6978  tfisi  7811  bropopvvv  8042  f1o2ndf1  8074  xpord3inddlem  8106  suppimacnv  8126  brovex  8174  tfrlem9  8326  tfrlem11  8329  odi  8516  nndi  8561  sbth  9037  sdomdif  9065  sbthfi  9135  zorn2lem7  10424  alephexp2  10504  addcanpi  10822  mulcanpi  10823  indpi  10830  prcdnq  10916  reclem2pr  10971  lediv2a  12048  nn01to3  12866  fi1uzind  14442  cshwlen  14734  cshwidxmodr  14739  rlimres  15493  ndvdssub  16348  bitsinv1  16381  nn0seqcvgd  16509  modprm0  16745  setsstruct  17115  initoeu2  17952  symgfixelsi  19376  symgfixfo  19380  uvcendim  21814  slesolex  22638  pm2mpf1  22755  mp2pm2mplem4  22765  fiinopn  22857  jensenlem2  26966  umgrupgr  29188  uspgrushgr  29262  uspgrupgr  29263  usgruspgr  29265  usgredg2vlem2  29311  cplgrop  29522  lfgrwlkprop  29771  2pthnloop  29816  usgr2pthlem  29848  elwwlks2  30054  clwlkclwwlklem2fv2  30083  eleclclwwlkn  30163  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  conngrv2edg  30282  3cyclfrgrrn1  30372  l2p  30566  strlem1  32337  ssiun2sf  32645  bnj981  35125  bnj1148  35171  swrdrevpfx  35330  consym1  36633  axc11n11  36920  bj-hbaeb2  37057  curryset  37185  currysetlem3  37188  bj-restb  37338  wl-axc11rc11  37827  clmgmOLD  38091  smgrpmgm  38104  smgrpassOLD  38105  grpomndo  38115  eldisjsim3  39177  aecom-o  39266  hbae-o  39268  hbequid  39274  equidqe  39287  equid1ALT  39290  axc11nfromc11  39291  ax12inda  39313  zindbi  43292  sdomne0  43758  exlimexi  44869  eexinst11  44872  e222  44981  e111  45019  e333  45077  stoweidlem34  46381  stoweidlem43  46390  funressnfv  47392  funbrafv  47507  ndmaovass  47555  tz6.12i-afv2  47592  dfatcolem  47604  ssfz12  47663  oexpnegnz  48027  fpprel2  48090  elclnbgrelnbgr  48174  grtriprop  48290  mgm2mgm  48576