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  122  impbid  202  ibi  256  anidms  677  3imp3i2an  1278  tbw-bijust  1623  tbw-negdf  1624  equid  1939  nf5di  2119  nfdiOLD  2225  hbae  2315  vtoclgaf  3271  vtocl2gaf  3273  vtocl3gaf  3275  vtocl4ga  3278  elinti  4485  copsexg  4956  vtoclr  5164  ssrelrn  5315  issref  5509  relresfld  5662  tz7.7  5749  elfvmptrab1  6305  tfisi  7058  bropopvvv  7255  f1o2ndf1  7285  suppimacnv  7306  brovex  7348  tfrlem9  7481  tfrlem11  7484  odi  7659  nndi  7703  sbth  8080  sdomdif  8108  zorn2lem7  9324  alephexp2  9403  addcanpi  9721  mulcanpi  9722  indpi  9729  prcdnq  9815  reclem2pr  9870  lediv2a  10917  nn01to3  11781  fi1uzind  13279  fi1uzindOLD  13285  cshwlen  13545  cshwidxmodr  13550  rlimres  14289  ndvdssub  15133  bitsinv1  15164  nn0seqcvgd  15283  modprm0  15510  setsstruct  15898  initoeu2  16666  symgfixelsi  17855  symgfixfo  17859  uvcendim  20186  slesolex  20488  pm2mpf1  20604  mp2pm2mplem4  20614  fiinopn  20706  jensenlem2  24714  umgrupgr  25998  uspgrushgr  26070  uspgrupgr  26071  usgruspgr  26073  usgredg2vlem2  26118  cplgrop  26333  lfgrwlkprop  26584  2pthnloop  26627  usgr2pthlem  26659  elwwlks2  26861  clwlkclwwlklem2fv2  26897  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  conngrv2edg  27055  frgrusgrfrcond  27123  3cyclfrgrrn1  27149  numclwlk1lem2foa  27224  l2p  27331  strlem1  29109  vtocl2d  29314  ssiun2sf  29378  bnj981  31020  bnj1148  31064  consym1  32419  axc11n11  32672  bj-hbaeb2  32805  bj-restb  33047  bj-ismoored0  33061  clmgmOLD  33650  smgrpmgm  33663  smgrpassOLD  33664  grpomndo  33674  aecom-o  34186  hbae-o  34188  hbequid  34194  equidqe  34207  equid1ALT  34210  axc11nfromc11  34211  ax12inda  34233  zindbi  37511  exlimexi  38730  eexinst11  38733  e222  38861  e111  38899  e333  38960  stoweidlem34  40251  stoweidlem43  40260  funressnfv  41208  funbrafv  41238  ndmaovass  41286  ssfz12  41324  oexpnegALTV  41588  oexpnegnz  41589  mgm2mgm  41863