Theorem ibi 270

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		ibi.1	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	1, 2	mpbid 235	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ibir  271  elab3gf  3641  elab3g  3642  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elpwi  4567  elsni  4604  elpri  4611  eltpi  4652  snssi  4749  prssi  4785  snelpwi  5423  prelpwi  5426  elxpi  5681  releldmb  5934  relelrnb  5935  elrnmpt2d  5954  eloni  6371  limuni2  6425  funeu  6562  fneu  6646  fvelima2  6934  fvelima  6947  fvelimad  6949  eloprabi  8064  fo2ndf  8122  orderseqlem  8159  tfrlem9  8378  oeeulem  8593  elqsi  8769  qsel  8800  ecopovsym  8823  elpmi  8849  elmapi  8852  pmsspw  8888  brdomi  8969  en0  9028  en0r  9030  en1  9034  mapdom1  9144  rexdif1en  9159  ominf  9238  unblem2  9267  unfilem1  9279  fodomfir  9301  fiin  9396  brwdomi  9544  canthwdom  9555  brwdom3i  9559  unxpwdom  9565  scott0b  9880  scott0OLD  9881  acni  10052  djuinf  10195  pwdjudom  10221  fin1ai  10299  fin2i  10301  fin4i  10304  ssfin3ds  10336  fin23lem17  10344  fin23lem38  10355  fin23lem39  10356  isfin32i  10371  fin34  10396  isfin7-2  10402  fin1a2lem13  10418  fin12  10419  gchi  10637  wuntr  10718  wununi  10719  wunpw  10720  wunpr  10722  wun0  10731  tskpwss  10765  tskpw  10766  tsken  10767  grutr  10806  grupw  10808  grupr  10810  gruurn  10811  ingru  10828  indpi  10920  eliooord  13462  fzrev3i  13650  fzne1  13663  elfzole1  13727  elfzolt2  13728  bcp1nk  14385  rere  15213  nn0abscl  15403  climcl  15590  rlimcl  15594  rlimdm  15642  o1res  15651  rlimdmo1  15709  climcau  15762  caucvgb  15771  fprodcnv  16076  cshws0  17199  restsspw  17522  mreiincl  17686  catidex  17768  catcocl  17779  catass  17780  homa1  18132  homahom2  18133  odulat  18529  dlatjmdi  18620  psrel  18663  psref2  18664  pstr2  18665  reldir  18693  dirdm  18694  dirref  18695  dirtr  18696  dirge  18697  chnub  18716  mgmcl  18739  submgmss  18813  submgmcl  18815  submgmmgm  18816  submss  18923  subm0cl  18925  submcl  18926  submmnd  18928  efmndbasf  18990  subgsubm  19278  symgbasf1o  19508  symginv  19535  psgneu  19639  odmulg  19689  frgpnabl  20008  dprdgrp  20140  dprdf  20141  abvfge0  20986  abveq0  20990  abvmul  20993  abvtri  20994  orngsqr  21038  lbsss  21267  lbssp  21269  lbsind  21270  domnchr  21751  cssi  21903  linds1  22029  linds2  22030  lindsind  22036  opsrtoslem2  22278  opsrso  22280  mdetunilem9  22848  uniopn  23128  iunopn  23129  inopn  23130  fiinopn  23132  eltpsg  23174  basis1  23181  basis2  23182  eltg4i  23191  lmff  23532  t1sep2  23600  cmpfii  23640  ptfinfin  23751  kqhmph  24051  fbasne0  24062  0nelfb  24063  fbsspw  24064  fbasssin  24068  ufli  24146  uffixfr  24155  elfm  24179  fclsopni  24247  fclselbas  24248  ustssxp  24437  ustbasel  24439  ustincl  24440  ustdiag  24441  ustinvel  24442  ustexhalf  24443  ustfilxp  24445  ustbas2  24457  ustbas  24459  psmetf  24538  psmet0  24540  psmettri2  24541  metflem  24560  xmetf  24561  xmeteq0  24570  xmettri2  24572  tmsxms  24718  tmsms  24719  metustsym  24787  tngnrg  24906  cncff  25127  cncfi  25128  cfili  25502  iscmet3lem2  25526  mbfres  25878  mbfimaopnlem  25889  limcresi  26119  dvcnp2  26154  ulmcl  26624  ulmf  26625  ulmcau  26638  pserulm  26665  pserdvlem2  26671  sinq34lt0t  26754  logtayl  26905  dchrmhm  27485  lgsdir2lem2  27570  2sqlem9  27671  mulog2sum  27781  newbdayim  28176  eleei  29362  uhgrf  29527  ushgrf  29528  upgrf  29551  umgrf  29563  uspgrf  29622  usgrf  29623  usgrfs  29625  nbcplgr  29902  clwlkcompim  30254  acycgrcycl  30640  tncp  30967  eulplig  30974  grpofo  30988  grpolidinv  30990  grpoass  30992  nvvop  31098  phpar  31313  pjch1  32159  nn0mnfxrd  33230  toslub  33421  tosglb  33423  suppgsumssiun  33520  exsslsb  34115  fldextsubrg  34167  fldextress  34169  zhmnrg  34483  issgon  34641  measfrge0  34722  measvnul  34725  measvun  34728  fzssfzo  35058  bnj916  35450  bnj983  35468  elkarden  35689  cplgredgex  35727  mfsdisj  36137  mtyf2  36138  maxsta  36141  mvtinf  36142  r1peuqusdeg1  36230  hfun  36766  hfsn  36767  hfelhf  36769  hfuni  36772  hfpw  36773  fneuni  36974  elttcirr  37158  curryset  37698  mptsnunlem  38100  heibor1lem  38567  heiborlem1  38569  heiborlem3  38571  opidonOLD  38610  isexid2  38613  elrelsrelim  39199  presucmap  39251  eqvrelqsel  39456  eldisjsim1  39690  elpcliN  40774  lnrfg  43968  sdomne0  44261  sdomne0d  44262  pwinfi2  44410  frege55lem1c  44764  gneispacef  44983  gneispacef2  44984  gneispacern2  44987  gneispace0nelrn  44988  gneispaceel  44991  gneispacess  44993  mnuop123d  45094  trintALTVD  45710  trintALT  45711  eliuniin  45939  eliuniin2  45960  disjrnmpt2  46028  stoweidlem35  46871  saluncl  47153  saldifcl  47155  0sal  47156  sge0resplit  47242  omedm  47335  funressneu  47943  afvelrnb0  48060  afvelima  48063  rlimdmafv  48073  funressndmafv2rn  48119  rlimdmafv2  48154  elsetpreimafv  48293  oexpnegALTV  48601  gricbri  48840  grlimprop2  48910  grilcbri  48933  asslawass  49116  linindsi  49385  inisegn0a  49772  eloprab1st2nd  49804  uobrcl  50127  uobeq2  50335  isinito2  50433  basrestermcfolem  50505  discsnterm  50508  islmd  50599