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  3608  elab3g  3609  elimhyp  4521  elimhyp2v  4522  elimhyp3v  4523  elimhyp4v  4524  elpwi  4539  elsni  4575  elpri  4580  eltpi  4620  snssi  4738  prssi  4751  prelpwi  5357  elxpi  5602  releldmb  5844  relelrnb  5845  elrnmpt2d  5861  eloni  6261  limuni2  6312  funeu  6443  fneu  6527  fvelima  6817  fvelimad  6818  eloprabi  7876  fo2ndf  7933  tfrlem9  8187  oeeulem  8394  elqsi  8517  qsel  8543  ecopovsym  8566  elpmi  8592  elmapi  8595  pmsspw  8623  brdomi  8704  en0  8758  en1  8765  undom  8800  mapdom1  8878  ominf  8964  unblem2  8997  unfilem1  9008  fiin  9111  brwdomi  9257  canthwdom  9268  brwdom3i  9272  unxpwdom  9278  scott0  9575  acni  9732  djuinf  9875  pwdjudom  9903  fin1ai  9980  fin2i  9982  fin4i  9985  ssfin3ds  10017  fin23lem17  10025  fin23lem38  10036  fin23lem39  10037  isfin32i  10052  fin34  10077  isfin7-2  10083  fin1a2lem13  10099  fin12  10100  gchi  10311  wuntr  10392  wununi  10393  wunpw  10394  wunpr  10396  wun0  10405  tskpwss  10439  tskpw  10440  tsken  10441  grutr  10480  grupw  10482  grupr  10484  gruurn  10485  ingru  10502  indpi  10594  eliooord  13067  fzrev3i  13252  elfzole1  13324  elfzolt2  13325  bcp1nk  13959  rere  14761  nn0abscl  14952  climcl  15136  rlimcl  15140  rlimdm  15188  o1res  15197  rlimdmo1  15255  climcau  15310  caucvgb  15319  fprodcnv  15621  cshws0  16731  restsspw  17059  mreiincl  17222  catidex  17300  catcocl  17311  catass  17312  homa1  17668  homahom2  17669  odulat  18068  dlatjmdi  18159  psrel  18202  psref2  18203  pstr2  18204  reldir  18232  dirdm  18233  dirref  18234  dirtr  18235  dirge  18236  mgmcl  18244  submss  18363  subm0cl  18365  submcl  18366  submmnd  18367  efmndbasf  18429  subgsubm  18692  symgbasf1o  18897  symginv  18925  psgneu  19029  odmulg  19078  frgpnabl  19391  dprdgrp  19523  dprdf  19524  abvfge0  19997  abveq0  20001  abvmul  20004  abvtri  20005  lbsss  20254  lbssp  20256  lbsind  20257  domnchr  20648  cssi  20801  linds1  20927  linds2  20928  lindsind  20934  opsrtoslem2  21173  opsrso  21175  mdetunilem9  21677  uniopn  21954  iunopn  21955  inopn  21956  fiinopn  21958  eltpsg  22000  eltpsgOLD  22001  basis1  22008  basis2  22009  eltg4i  22018  lmff  22360  t1sep2  22428  cmpfii  22468  ptfinfin  22578  kqhmph  22878  fbasne0  22889  0nelfb  22890  fbsspw  22891  fbasssin  22895  ufli  22973  uffixfr  22982  elfm  23006  fclsopni  23074  fclselbas  23075  ustssxp  23264  ustbasel  23266  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ustfilxp  23272  ustbas2  23285  ustbas  23287  psmetf  23367  psmet0  23369  psmettri2  23370  metflem  23389  xmetf  23390  xmeteq0  23399  xmettri2  23401  tmsxms  23548  tmsms  23549  metustsym  23617  tngnrg  23744  cncff  23962  cncfi  23963  cfili  24337  iscmet3lem2  24361  mbfres  24713  mbfimaopnlem  24724  limcresi  24954  dvcnp2  24989  ulmcl  25445  ulmf  25446  ulmcau  25459  pserulm  25486  pserdvlem2  25492  sinq34lt0t  25571  logtayl  25720  dchrmhm  26294  lgsdir2lem2  26379  2sqlem9  26480  mulog2sum  26590  eleei  27168  uhgrf  27335  ushgrf  27336  upgrf  27359  umgrf  27371  uspgrf  27427  usgrf  27428  usgrfs  27430  nbcplgr  27704  clwlkcompim  28049  tncp  28741  eulplig  28748  grpofo  28762  grpolidinv  28764  grpoass  28766  nvvop  28872  phpar  29087  pjch1  29933  fzne1  31011  toslub  31153  tosglb  31155  orngsqr  31405  fldextsubrg  31628  fldextress  31629  zhmnrg  31817  issgon  31991  measfrge0  32071  measvnul  32074  measvun  32077  fzssfzo  32418  bnj916  32813  bnj983  32831  cplgredgex  32982  acycgrcycl  33009  mfsdisj  33412  mtyf2  33413  maxsta  33416  mvtinf  33417  orderseqlem  33728  hfun  34407  hfsn  34408  hfelhf  34410  hfuni  34413  hfpw  34414  fneuni  34463  curryset  35062  mptsnunlem  35436  heibor1lem  35894  heiborlem1  35896  heiborlem3  35898  opidonOLD  35937  isexid2  35940  elrelsrelim  36533  eqvrelqsel  36656  elpcliN  37834  lnrfg  40860  pwinfi2  41058  frege55lem1c  41413  gneispacef  41634  gneispacef2  41635  gneispacern2  41638  gneispace0nelrn  41639  gneispaceel  41642  gneispacess  41644  mnuop123d  41769  trintALTVD  42389  trintALT  42390  eliuniin  42538  eliuniin2  42558  disjrnmpt2  42615  fvelima2  42695  stoweidlem35  43466  saluncl  43748  saldifcl  43750  0sal  43751  sge0resplit  43834  omedm  43927  funressneu  44428  afvelrnb0  44543  afvelima  44546  rlimdmafv  44556  funressndmafv2rn  44602  rlimdmafv2  44637  elsetpreimafv  44725  oexpnegALTV  45017  isisomgr  45164  submgmss  45234  submgmcl  45236  submgmmgm  45237  asslawass  45275  linindsi  45676