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  3639  elab3g  3640  elimhyp  4545  elimhyp2v  4546  elimhyp3v  4547  elimhyp4v  4548  elpwi  4561  elsni  4597  elpri  4604  eltpi  4645  snssi  4764  prssi  4777  snelpwi  5392  prelpwi  5395  elxpi  5646  releldmb  5895  relelrnb  5896  elrnmpt2d  5915  eloni  6327  limuni2  6380  funeu  6517  fneu  6602  fvelima2  6886  fvelima  6899  fvelimad  6901  eloprabi  8007  fo2ndf  8063  orderseqlem  8099  tfrlem9  8316  oeeulem  8529  elqsi  8703  qsel  8733  ecopovsym  8756  elpmi  8783  elmapi  8786  pmsspw  8815  brdomi  8896  en0  8955  en0r  8957  en1  8961  mapdom1  9070  rexdif1en  9085  ominf  9164  unblem2  9193  unfilem1  9205  fodomfir  9228  fiin  9325  brwdomi  9473  canthwdom  9484  brwdom3i  9488  unxpwdom  9494  scott0  9798  acni  9955  djuinf  10099  pwdjudom  10125  fin1ai  10203  fin2i  10205  fin4i  10208  ssfin3ds  10240  fin23lem17  10248  fin23lem38  10259  fin23lem39  10260  isfin32i  10275  fin34  10300  isfin7-2  10306  fin1a2lem13  10322  fin12  10323  gchi  10535  wuntr  10616  wununi  10617  wunpw  10618  wunpr  10620  wun0  10629  tskpwss  10663  tskpw  10664  tsken  10665  grutr  10704  grupw  10706  grupr  10708  gruurn  10709  ingru  10726  indpi  10818  eliooord  13321  fzrev3i  13507  fzne1  13520  elfzole1  13583  elfzolt2  13584  bcp1nk  14240  rere  15045  nn0abscl  15235  climcl  15422  rlimcl  15426  rlimdm  15474  o1res  15483  rlimdmo1  15541  climcau  15594  caucvgb  15603  fprodcnv  15906  cshws0  17029  restsspw  17351  mreiincl  17515  catidex  17597  catcocl  17608  catass  17609  homa1  17961  homahom2  17962  odulat  18358  dlatjmdi  18449  psrel  18492  psref2  18493  pstr2  18494  reldir  18522  dirdm  18523  dirref  18524  dirtr  18525  dirge  18526  chnub  18545  mgmcl  18568  submgmss  18630  submgmcl  18632  submgmmgm  18633  submss  18734  subm0cl  18736  submcl  18737  submmnd  18738  efmndbasf  18800  subgsubm  19078  symgbasf1o  19304  symginv  19331  psgneu  19435  odmulg  19485  frgpnabl  19804  dprdgrp  19936  dprdf  19937  abvfge0  20747  abveq0  20751  abvmul  20754  abvtri  20755  orngsqr  20799  lbsss  21029  lbssp  21031  lbsind  21032  domnchr  21487  cssi  21639  linds1  21765  linds2  21766  lindsind  21772  opsrtoslem2  22011  opsrso  22013  mdetunilem9  22564  uniopn  22841  iunopn  22842  inopn  22843  fiinopn  22845  eltpsg  22887  basis1  22894  basis2  22895  eltg4i  22904  lmff  23245  t1sep2  23313  cmpfii  23353  ptfinfin  23463  kqhmph  23763  fbasne0  23774  0nelfb  23775  fbsspw  23776  fbasssin  23780  ufli  23858  uffixfr  23867  elfm  23891  fclsopni  23959  fclselbas  23960  ustssxp  24149  ustbasel  24151  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  ustfilxp  24157  ustbas2  24169  ustbas  24171  psmetf  24250  psmet0  24252  psmettri2  24253  metflem  24272  xmetf  24273  xmeteq0  24282  xmettri2  24284  tmsxms  24430  tmsms  24431  metustsym  24499  tngnrg  24618  cncff  24842  cncfi  24843  cfili  25224  iscmet3lem2  25248  mbfres  25601  mbfimaopnlem  25612  limcresi  25842  dvcnp2  25877  dvcnp2OLD  25878  ulmcl  26346  ulmf  26347  ulmcau  26360  pserulm  26387  pserdvlem2  26394  sinq34lt0t  26474  logtayl  26625  dchrmhm  27208  lgsdir2lem2  27293  2sqlem9  27394  mulog2sum  27504  newbdayim  27899  eleei  28970  uhgrf  29135  ushgrf  29136  upgrf  29159  umgrf  29171  uspgrf  29227  usgrf  29228  usgrfs  29230  nbcplgr  29507  clwlkcompim  29853  tncp  30553  eulplig  30560  grpofo  30574  grpolidinv  30576  grpoass  30578  nvvop  30684  phpar  30899  pjch1  31745  nn0mnfxrd  32831  toslub  33055  tosglb  33057  exsslsb  33753  fldextsubrg  33806  fldextress  33808  zhmnrg  34122  issgon  34280  measfrge0  34360  measvnul  34363  measvun  34366  fzssfzo  34696  bnj916  35089  bnj983  35107  cplgredgex  35315  acycgrcycl  35341  mfsdisj  35744  mtyf2  35745  maxsta  35748  mvtinf  35749  r1peuqusdeg1  35837  hfun  36372  hfsn  36373  hfelhf  36375  hfuni  36378  hfpw  36379  fneuni  36541  curryset  37147  mptsnunlem  37543  heibor1lem  38010  heiborlem1  38012  heiborlem3  38014  opidonOLD  38053  isexid2  38056  elrelsrelim  38628  presucmap  38668  eqvrelqsel  38873  elpcliN  40153  lnrfg  43361  sdomne0  43654  sdomne0d  43655  pwinfi2  43803  frege55lem1c  44157  gneispacef  44376  gneispacef2  44377  gneispacern2  44380  gneispace0nelrn  44381  gneispaceel  44384  gneispacess  44386  mnuop123d  44503  trintALTVD  45120  trintALT  45121  eliuniin  45343  eliuniin2  45364  disjrnmpt2  45432  stoweidlem35  46279  saluncl  46561  saldifcl  46563  0sal  46564  sge0resplit  46650  omedm  46743  funressneu  47293  afvelrnb0  47410  afvelima  47413  rlimdmafv  47423  funressndmafv2rn  47469  rlimdmafv2  47504  elsetpreimafv  47631  oexpnegALTV  47923  gricbri  48162  grlimprop2  48232  grilcbri  48255  asslawass  48439  linindsi  48693  inisegn0a  49081  eloprab1st2nd  49113  uobrcl  49438  uobeq2  49646  isinito2  49744  basrestermcfolem  49816  discsnterm  49819  islmd  49910