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  1699  tbw-negdf  1700  equid  2013  nf5di  2289  hbae  2433  vtoclgaf  3529  vtoclga  3530  vtocl2gafOLD  3533  vtocl3gafOLD  3535  vtocl3gaOLD  3537  vtocl4gaOLD  3540  elinti  4908  copsexgw  5435  copsexg  5436  vtoclr  5684  ssrelrn  5841  relresfld  6231  tz7.7  6340  elfvunirn  6861  elfvmptrab1  6966  tfisi  7798  bropopvvv  8029  f1o2ndf1  8061  xpord3inddlem  8093  suppimacnv  8113  brovex  8161  tfrlem9  8313  tfrlem11  8316  odi  8503  nndi  8547  sbth  9020  sdomdif  9048  sbthfi  9118  zorn2lem7  10403  alephexp2  10482  addcanpi  10800  mulcanpi  10801  indpi  10808  prcdnq  10894  reclem2pr  10949  lediv2a  12026  nn01to3  12849  fi1uzind  14424  cshwlen  14716  cshwidxmodr  14721  rlimres  15475  ndvdssub  16330  bitsinv1  16363  nn0seqcvgd  16491  modprm0  16727  setsstruct  17097  initoeu2  17933  symgfixelsi  19357  symgfixfo  19361  uvcendim  21794  slesolex  22607  pm2mpf1  22724  mp2pm2mplem4  22734  fiinopn  22826  jensenlem2  26935  umgrupgr  29092  uspgrushgr  29166  uspgrupgr  29167  usgruspgr  29169  usgredg2vlem2  29215  cplgrop  29426  lfgrwlkprop  29675  2pthnloop  29720  usgr2pthlem  29752  elwwlks2  29958  clwlkclwwlklem2fv2  29987  eleclclwwlkn  30067  hashecclwwlkn1  30068  umgrhashecclwwlk  30069  conngrv2edg  30186  3cyclfrgrrn1  30276  l2p  30470  strlem1  32241  ssiun2sf  32550  bnj981  34973  bnj1148  35019  swrdrevpfx  35172  consym1  36475  axc11n11  36737  bj-hbaeb2  36873  curryset  37001  currysetlem3  37004  bj-restb  37149  wl-axc11rc11  37638  clmgmOLD  37901  smgrpmgm  37914  smgrpassOLD  37915  grpomndo  37925  aecom-o  39010  hbae-o  39012  hbequid  39018  equidqe  39031  equid1ALT  39034  axc11nfromc11  39035  ax12inda  39057  zindbi  43053  sdomne0  43520  exlimexi  44631  eexinst11  44634  e222  44743  e111  44781  e333  44839  stoweidlem34  46146  stoweidlem43  46155  funressnfv  47157  funbrafv  47272  ndmaovass  47320  tz6.12i-afv2  47357  dfatcolem  47369  ssfz12  47428  oexpnegnz  47792  fpprel2  47855  elclnbgrelnbgr  47939  grtriprop  48055  mgm2mgm  48341