Theorem ibi 267

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 232	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ibir  268  elab3gf  3636  elab3g  3637  elimhyp  4542  elimhyp2v  4543  elimhyp3v  4544  elimhyp4v  4545  elpwi  4558  elsni  4594  elpri  4601  eltpi  4642  snssi  4761  prssi  4774  snelpwi  5389  prelpwi  5392  elxpi  5643  releldmb  5892  relelrnb  5893  elrnmpt2d  5912  eloni  6323  limuni2  6376  funeu  6513  fneu  6598  fvelima2  6882  fvelima  6895  fvelimad  6897  eloprabi  8003  fo2ndf  8059  orderseqlem  8095  tfrlem9  8312  oeeulem  8524  elqsi  8698  qsel  8728  ecopovsym  8751  elpmi  8778  elmapi  8781  pmsspw  8809  brdomi  8890  en0  8949  en0r  8951  en1  8955  mapdom1  9064  rexdif1en  9079  ominf  9157  unblem2  9186  unfilem1  9198  fodomfir  9221  fiin  9315  brwdomi  9463  canthwdom  9474  brwdom3i  9478  unxpwdom  9484  scott0  9788  acni  9945  djuinf  10089  pwdjudom  10115  fin1ai  10193  fin2i  10195  fin4i  10198  ssfin3ds  10230  fin23lem17  10238  fin23lem38  10249  fin23lem39  10250  isfin32i  10265  fin34  10290  isfin7-2  10296  fin1a2lem13  10312  fin12  10313  gchi  10524  wuntr  10605  wununi  10606  wunpw  10607  wunpr  10609  wun0  10618  tskpwss  10652  tskpw  10653  tsken  10654  grutr  10693  grupw  10695  grupr  10697  gruurn  10698  ingru  10715  indpi  10807  eliooord  13309  fzrev3i  13495  fzne1  13508  elfzole1  13571  elfzolt2  13572  bcp1nk  14228  rere  15033  nn0abscl  15223  climcl  15410  rlimcl  15414  rlimdm  15462  o1res  15471  rlimdmo1  15529  climcau  15582  caucvgb  15591  fprodcnv  15894  cshws0  17017  restsspw  17339  mreiincl  17502  catidex  17584  catcocl  17595  catass  17596  homa1  17948  homahom2  17949  odulat  18345  dlatjmdi  18436  psrel  18479  psref2  18480  pstr2  18481  reldir  18509  dirdm  18510  dirref  18511  dirtr  18512  dirge  18513  chnub  18532  mgmcl  18555  submgmss  18617  submgmcl  18619  submgmmgm  18620  submss  18721  subm0cl  18723  submcl  18724  submmnd  18725  efmndbasf  18787  subgsubm  19065  symgbasf1o  19291  symginv  19318  psgneu  19422  odmulg  19472  frgpnabl  19791  dprdgrp  19923  dprdf  19924  abvfge0  20733  abveq0  20737  abvmul  20740  abvtri  20741  orngsqr  20785  lbsss  21015  lbssp  21017  lbsind  21018  domnchr  21473  cssi  21625  linds1  21751  linds2  21752  lindsind  21758  opsrtoslem2  21994  opsrso  21996  mdetunilem9  22538  uniopn  22815  iunopn  22816  inopn  22817  fiinopn  22819  eltpsg  22861  basis1  22868  basis2  22869  eltg4i  22878  lmff  23219  t1sep2  23287  cmpfii  23327  ptfinfin  23437  kqhmph  23737  fbasne0  23748  0nelfb  23749  fbsspw  23750  fbasssin  23754  ufli  23832  uffixfr  23841  elfm  23865  fclsopni  23933  fclselbas  23934  ustssxp  24123  ustbasel  24125  ustincl  24126  ustdiag  24127  ustinvel  24128  ustexhalf  24129  ustfilxp  24131  ustbas2  24143  ustbas  24145  psmetf  24224  psmet0  24226  psmettri2  24227  metflem  24246  xmetf  24247  xmeteq0  24256  xmettri2  24258  tmsxms  24404  tmsms  24405  metustsym  24473  tngnrg  24592  cncff  24816  cncfi  24817  cfili  25198  iscmet3lem2  25222  mbfres  25575  mbfimaopnlem  25586  limcresi  25816  dvcnp2  25851  dvcnp2OLD  25852  ulmcl  26320  ulmf  26321  ulmcau  26334  pserulm  26361  pserdvlem2  26368  sinq34lt0t  26448  logtayl  26599  dchrmhm  27182  lgsdir2lem2  27267  2sqlem9  27368  mulog2sum  27478  newbdayim  27851  eleei  28879  uhgrf  29044  ushgrf  29045  upgrf  29068  umgrf  29080  uspgrf  29136  usgrf  29137  usgrfs  29139  nbcplgr  29416  clwlkcompim  29762  tncp  30462  eulplig  30469  grpofo  30483  grpolidinv  30485  grpoass  30487  nvvop  30593  phpar  30808  pjch1  31654  toslub  32963  tosglb  32965  exsslsb  33632  fldextsubrg  33685  fldextress  33687  zhmnrg  34001  issgon  34159  measfrge0  34239  measvnul  34242  measvun  34245  fzssfzo  34575  bnj916  34968  bnj983  34986  cplgredgex  35188  acycgrcycl  35214  mfsdisj  35617  mtyf2  35618  maxsta  35621  mvtinf  35622  r1peuqusdeg1  35710  hfun  36245  hfsn  36246  hfelhf  36248  hfuni  36251  hfpw  36252  fneuni  36414  curryset  37013  mptsnunlem  37405  heibor1lem  37872  heiborlem1  37874  heiborlem3  37876  opidonOLD  37915  isexid2  37918  elrelsrelim  38490  presucmap  38530  eqvrelqsel  38735  elpcliN  40015  lnrfg  43239  sdomne0  43533  sdomne0d  43534  pwinfi2  43682  frege55lem1c  44036  gneispacef  44255  gneispacef2  44256  gneispacern2  44259  gneispace0nelrn  44260  gneispaceel  44263  gneispacess  44265  mnuop123d  44382  trintALTVD  44999  trintALT  45000  eliuniin  45223  eliuniin2  45244  disjrnmpt2  45312  stoweidlem35  46160  saluncl  46442  saldifcl  46444  0sal  46445  sge0resplit  46531  omedm  46624  funressneu  47174  afvelrnb0  47291  afvelima  47294  rlimdmafv  47304  funressndmafv2rn  47350  rlimdmafv2  47385  elsetpreimafv  47512  oexpnegALTV  47804  gricbri  48043  grlimprop2  48113  grilcbri  48136  asslawass  48320  linindsi  48575  inisegn0a  48963  eloprab1st2nd  48995  uobrcl  49321  uobeq2  49529  isinito2  49627  basrestermcfolem  49699  discsnterm  49702  islmd  49793