Theorem ibi 266

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)

Hypothesis

Ref	Expression
ibi.1	⊢ (𝜑 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ibi	⊢ (𝜑 → 𝜓)

Proof of Theorem ibi

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		ibi.1	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	1, 2	mpbid 231	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  ibir  267  elab3gf  3671  elab3g  3672  elimhyp  4588  elimhyp2v  4589  elimhyp3v  4590  elimhyp4v  4591  elpwi  4604  elsni  4640  elpri  4646  eltpi  4686  snssi  4807  prssi  4820  snelpwi  5441  prelpwi  5445  elxpi  5696  releldmb  5944  relelrnb  5945  elrnmpt2d  5962  eloni  6378  limuni2  6430  funeu  6576  fneu  6662  fvelima  6960  fvelimad  6962  eloprabi  8069  fo2ndf  8127  orderseqlem  8163  tfrlem9  8407  oeeulem  8623  elqsi  8791  qsel  8817  ecopovsym  8840  elpmi  8867  elmapi  8870  pmsspw  8898  brdomi  8981  brdomiOLD  8982  en0  9041  en0r  9044  en1  9049  undomOLD  9090  mapdom1  9172  rexdif1en  9188  ominf  9285  ominfOLD  9286  unblem2  9323  unfilem1  9337  fodomfir  9363  fiin  9458  brwdomi  9604  canthwdom  9615  brwdom3i  9619  unxpwdom  9625  scott0  9922  acni  10081  djuinf  10224  pwdjudom  10250  fin1ai  10327  fin2i  10329  fin4i  10332  ssfin3ds  10364  fin23lem17  10372  fin23lem38  10383  fin23lem39  10384  isfin32i  10399  fin34  10424  isfin7-2  10430  fin1a2lem13  10446  fin12  10447  gchi  10658  wuntr  10739  wununi  10740  wunpw  10741  wunpr  10743  wun0  10752  tskpwss  10786  tskpw  10787  tsken  10788  grutr  10827  grupw  10829  grupr  10831  gruurn  10832  ingru  10849  indpi  10941  eliooord  13431  fzrev3i  13616  elfzole1  13688  elfzolt2  13689  bcp1nk  14329  rere  15122  nn0abscl  15312  climcl  15496  rlimcl  15500  rlimdm  15548  o1res  15557  rlimdmo1  15615  climcau  15670  caucvgb  15679  fprodcnv  15980  cshws0  17099  restsspw  17441  mreiincl  17604  catidex  17682  catcocl  17693  catass  17694  homa1  18054  homahom2  18055  odulat  18455  dlatjmdi  18546  psrel  18589  psref2  18590  pstr2  18591  reldir  18619  dirdm  18620  dirref  18621  dirtr  18622  dirge  18623  mgmcl  18631  submgmss  18693  submgmcl  18695  submgmmgm  18696  submss  18794  subm0cl  18796  submcl  18797  submmnd  18798  efmndbasf  18860  subgsubm  19138  symgbasf1o  19368  symginv  19396  psgneu  19500  odmulg  19550  frgpnabl  19869  dprdgrp  20001  dprdf  20002  abvfge0  20789  abveq0  20793  abvmul  20796  abvtri  20797  lbsss  21051  lbssp  21053  lbsind  21054  domnchr  21522  cssi  21676  linds1  21804  linds2  21805  lindsind  21811  opsrtoslem2  22065  opsrso  22067  mdetunilem9  22610  uniopn  22887  iunopn  22888  inopn  22889  fiinopn  22891  eltpsg  22933  eltpsgOLD  22934  basis1  22941  basis2  22942  eltg4i  22951  lmff  23293  t1sep2  23361  cmpfii  23401  ptfinfin  23511  kqhmph  23811  fbasne0  23822  0nelfb  23823  fbsspw  23824  fbasssin  23828  ufli  23906  uffixfr  23915  elfm  23939  fclsopni  24007  fclselbas  24008  ustssxp  24197  ustbasel  24199  ustincl  24200  ustdiag  24201  ustinvel  24202  ustexhalf  24203  ustfilxp  24205  ustbas2  24218  ustbas  24220  psmetf  24300  psmet0  24302  psmettri2  24303  metflem  24322  xmetf  24323  xmeteq0  24332  xmettri2  24334  tmsxms  24483  tmsms  24484  metustsym  24552  tngnrg  24679  cncff  24901  cncfi  24902  cfili  25284  iscmet3lem2  25308  mbfres  25661  mbfimaopnlem  25672  limcresi  25902  dvcnp2  25937  dvcnp2OLD  25938  ulmcl  26407  ulmf  26408  ulmcau  26421  pserulm  26448  pserdvlem2  26455  sinq34lt0t  26534  logtayl  26684  dchrmhm  27267  lgsdir2lem2  27352  2sqlem9  27453  mulog2sum  27563  eleei  28828  uhgrf  28995  ushgrf  28996  upgrf  29019  umgrf  29031  uspgrf  29087  usgrf  29088  usgrfs  29090  nbcplgr  29367  clwlkcompim  29714  tncp  30408  eulplig  30415  grpofo  30429  grpolidinv  30431  grpoass  30433  nvvop  30539  phpar  30754  pjch1  31600  fzne1  32693  toslub  32846  tosglb  32848  chnub  32884  orngsqr  33187  fldextsubrg  33546  fldextress  33547  zhmnrg  33795  issgon  33969  measfrge0  34049  measvnul  34052  measvun  34055  fzssfzo  34398  bnj916  34791  bnj983  34809  cplgredgex  34961  acycgrcycl  34988  mfsdisj  35391  mtyf2  35392  maxsta  35395  mvtinf  35396  r1peuqusdeg1  35484  hfun  36015  hfsn  36016  hfelhf  36018  hfuni  36021  hfpw  36022  fneuni  36072  curryset  36666  mptsnunlem  37058  heibor1lem  37523  heiborlem1  37525  heiborlem3  37527  opidonOLD  37566  isexid2  37569  elrelsrelim  38199  eqvrelqsel  38327  elpcliN  39605  lnrfg  42817  sdomne0  43117  sdomne0d  43118  pwinfi2  43266  frege55lem1c  43620  gneispacef  43839  gneispacef2  43840  gneispacern2  43843  gneispace0nelrn  43844  gneispaceel  43847  gneispacess  43849  mnuop123d  43973  trintALTVD  44593  trintALT  44594  eliuniin  44737  eliuniin2  44758  disjrnmpt2  44831  fvelima2  44905  stoweidlem35  45692  saluncl  45974  saldifcl  45976  0sal  45977  sge0resplit  46063  omedm  46156  funressneu  46698  afvelrnb0  46813  afvelima  46816  rlimdmafv  46826  funressndmafv2rn  46872  rlimdmafv2  46907  elsetpreimafv  46993  oexpnegALTV  47285  gricbri  47500  grlimprop2  47528  grilcbri  47535  asslawass  47606  linindsi  47866