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  3684  elab3g  3685  elimhyp  4591  elimhyp2v  4592  elimhyp3v  4593  elimhyp4v  4594  elpwi  4607  elsni  4643  elpri  4649  eltpi  4688  snssi  4808  prssi  4821  snelpwi  5448  prelpwi  5452  elxpi  5707  releldmb  5957  relelrnb  5958  elrnmpt2d  5977  eloni  6394  limuni2  6446  funeu  6591  fneu  6678  fvelima2  6961  fvelima  6974  fvelimad  6976  eloprabi  8088  fo2ndf  8146  orderseqlem  8182  tfrlem9  8425  oeeulem  8639  elqsi  8810  qsel  8836  ecopovsym  8859  elpmi  8886  elmapi  8889  pmsspw  8917  brdomi  8999  brdomiOLD  9000  en0  9058  en0r  9060  en1  9064  undomOLD  9100  mapdom1  9182  rexdif1en  9198  ominf  9294  ominfOLD  9295  unblem2  9329  unfilem1  9343  fodomfir  9368  fiin  9462  brwdomi  9608  canthwdom  9619  brwdom3i  9623  unxpwdom  9629  scott0  9926  acni  10085  djuinf  10229  pwdjudom  10255  fin1ai  10333  fin2i  10335  fin4i  10338  ssfin3ds  10370  fin23lem17  10378  fin23lem38  10389  fin23lem39  10390  isfin32i  10405  fin34  10430  isfin7-2  10436  fin1a2lem13  10452  fin12  10453  gchi  10664  wuntr  10745  wununi  10746  wunpw  10747  wunpr  10749  wun0  10758  tskpwss  10792  tskpw  10793  tsken  10794  grutr  10833  grupw  10835  grupr  10837  gruurn  10838  ingru  10855  indpi  10947  eliooord  13446  fzrev3i  13631  fzne1  13644  elfzole1  13707  elfzolt2  13708  bcp1nk  14356  rere  15161  nn0abscl  15351  climcl  15535  rlimcl  15539  rlimdm  15587  o1res  15596  rlimdmo1  15654  climcau  15707  caucvgb  15716  fprodcnv  16019  cshws0  17139  restsspw  17476  mreiincl  17639  catidex  17717  catcocl  17728  catass  17729  homa1  18082  homahom2  18083  odulat  18480  dlatjmdi  18571  psrel  18614  psref2  18615  pstr2  18616  reldir  18644  dirdm  18645  dirref  18646  dirtr  18647  dirge  18648  mgmcl  18656  submgmss  18718  submgmcl  18720  submgmmgm  18721  submss  18822  subm0cl  18824  submcl  18825  submmnd  18826  efmndbasf  18888  subgsubm  19166  symgbasf1o  19392  symginv  19420  psgneu  19524  odmulg  19574  frgpnabl  19893  dprdgrp  20025  dprdf  20026  abvfge0  20815  abveq0  20819  abvmul  20822  abvtri  20823  lbsss  21076  lbssp  21078  lbsind  21079  domnchr  21547  cssi  21702  linds1  21830  linds2  21831  lindsind  21837  opsrtoslem2  22080  opsrso  22082  mdetunilem9  22626  uniopn  22903  iunopn  22904  inopn  22905  fiinopn  22907  eltpsg  22949  eltpsgOLD  22950  basis1  22957  basis2  22958  eltg4i  22967  lmff  23309  t1sep2  23377  cmpfii  23417  ptfinfin  23527  kqhmph  23827  fbasne0  23838  0nelfb  23839  fbsspw  23840  fbasssin  23844  ufli  23922  uffixfr  23931  elfm  23955  fclsopni  24023  fclselbas  24024  ustssxp  24213  ustbasel  24215  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  ustfilxp  24221  ustbas2  24234  ustbas  24236  psmetf  24316  psmet0  24318  psmettri2  24319  metflem  24338  xmetf  24339  xmeteq0  24348  xmettri2  24350  tmsxms  24499  tmsms  24500  metustsym  24568  tngnrg  24695  cncff  24919  cncfi  24920  cfili  25302  iscmet3lem2  25326  mbfres  25679  mbfimaopnlem  25690  limcresi  25920  dvcnp2  25955  dvcnp2OLD  25956  ulmcl  26424  ulmf  26425  ulmcau  26438  pserulm  26465  pserdvlem2  26472  sinq34lt0t  26551  logtayl  26702  dchrmhm  27285  lgsdir2lem2  27370  2sqlem9  27471  mulog2sum  27581  eleei  28912  uhgrf  29079  ushgrf  29080  upgrf  29103  umgrf  29115  uspgrf  29171  usgrf  29172  usgrfs  29174  nbcplgr  29451  clwlkcompim  29800  tncp  30497  eulplig  30504  grpofo  30518  grpolidinv  30520  grpoass  30522  nvvop  30628  phpar  30843  pjch1  31689  toslub  32963  tosglb  32965  chnub  33002  orngsqr  33334  exsslsb  33647  fldextsubrg  33702  fldextress  33703  zhmnrg  33966  issgon  34124  measfrge0  34204  measvnul  34207  measvun  34210  fzssfzo  34554  bnj916  34947  bnj983  34965  cplgredgex  35126  acycgrcycl  35152  mfsdisj  35555  mtyf2  35556  maxsta  35559  mvtinf  35560  r1peuqusdeg1  35648  hfun  36179  hfsn  36180  hfelhf  36182  hfuni  36185  hfpw  36186  fneuni  36348  curryset  36947  mptsnunlem  37339  heibor1lem  37816  heiborlem1  37818  heiborlem3  37820  opidonOLD  37859  isexid2  37862  elrelsrelim  38489  eqvrelqsel  38617  elpcliN  39895  lnrfg  43131  sdomne0  43426  sdomne0d  43427  pwinfi2  43575  frege55lem1c  43929  gneispacef  44148  gneispacef2  44149  gneispacern2  44152  gneispace0nelrn  44153  gneispaceel  44156  gneispacess  44158  mnuop123d  44281  trintALTVD  44900  trintALT  44901  eliuniin  45104  eliuniin2  45125  disjrnmpt2  45193  stoweidlem35  46050  saluncl  46332  saldifcl  46334  0sal  46335  sge0resplit  46421  omedm  46514  funressneu  47059  afvelrnb0  47176  afvelima  47179  rlimdmafv  47189  funressndmafv2rn  47235  rlimdmafv2  47270  elsetpreimafv  47372  oexpnegALTV  47664  gricbri  47885  grlimprop2  47953  grilcbri  47969  asslawass  48109  linindsi  48364