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.18OLD  129  impbid  214  anidms  569  tbw-bijust  1695  tbw-negdf  1696  equid  2015  nf5di  2289  hbae  2449  vtoclgaf  3573  vtoclga  3574  vtocl2gaf  3576  vtocl3gaf  3577  vtocl4ga  3580  vtocl2dOLD  3931  elinti  4878  copsexgw  5374  copsexg  5375  vtoclr  5610  ssrelrn  5758  relresfld  6122  tz7.7  6212  elfvmptrab1  6790  tfisi  7567  bropopvvv  7779  f1o2ndf1  7812  suppimacnv  7835  brovex  7882  tfrlem9  8015  tfrlem11  8018  odi  8199  nndi  8243  sbth  8631  sdomdif  8659  zorn2lem7  9918  alephexp2  9997  addcanpi  10315  mulcanpi  10316  indpi  10323  prcdnq  10409  reclem2pr  10464  lediv2a  11528  nn01to3  12335  fi1uzind  13849  cshwlen  14155  cshwidxmodr  14160  rlimres  14909  ndvdssub  15754  bitsinv1  15785  nn0seqcvgd  15908  modprm0  16136  setsstruct  16517  initoeu2  17270  symgfixelsi  18557  symgfixfo  18561  uvcendim  20985  slesolex  21285  pm2mpf1  21401  mp2pm2mplem4  21411  fiinopn  21503  jensenlem2  25559  umgrupgr  26882  uspgrushgr  26954  uspgrupgr  26955  usgruspgr  26957  usgredg2vlem2  27002  cplgrop  27213  lfgrwlkprop  27463  2pthnloop  27506  usgr2pthlem  27538  elwwlks2  27739  clwlkclwwlklem2fv2  27768  eleclclwwlkn  27849  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  conngrv2edg  27968  3cyclfrgrrn1  28058  l2p  28250  strlem1  30021  ssiun2sf  30305  bnj981  32217  bnj1148  32263  swrdrevpfx  32358  consym1  33763  axc11n11  34011  bj-hbaeb2  34136  curryset  34252  currysetlem3  34255  bj-restb  34379  wl-axc11rc11  34809  clmgmOLD  35123  smgrpmgm  35136  smgrpassOLD  35137  grpomndo  35147  aecom-o  36031  hbae-o  36033  hbequid  36039  equidqe  36052  equid1ALT  36055  axc11nfromc11  36056  ax12inda  36078  zindbi  39536  exlimexi  40851  eexinst11  40854  e222  40963  e111  41001  e333  41060  stoweidlem34  42312  stoweidlem43  42321  funressnfv  43271  funbrafv  43350  ndmaovass  43398  tz6.12i-afv2  43435  dfatcolem  43447  ssfz12  43507  oexpnegnz  43836  fpprel2  43899  mgm2mgm  44127