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  3700  elab3g  3701  elimhyp  4613  elimhyp2v  4614  elimhyp3v  4615  elimhyp4v  4616  elpwi  4629  elsni  4665  elpri  4671  eltpi  4711  snssi  4833  prssi  4846  snelpwi  5463  prelpwi  5467  elxpi  5722  releldmb  5971  relelrnb  5972  elrnmpt2d  5989  eloni  6405  limuni2  6457  funeu  6603  fneu  6689  fvelima  6987  fvelimad  6989  eloprabi  8104  fo2ndf  8162  orderseqlem  8198  tfrlem9  8441  oeeulem  8657  elqsi  8828  qsel  8854  ecopovsym  8877  elpmi  8904  elmapi  8907  pmsspw  8935  brdomi  9018  brdomiOLD  9019  en0  9078  en0r  9081  en1  9086  undomOLD  9126  mapdom1  9208  rexdif1en  9224  ominf  9321  ominfOLD  9322  unblem2  9357  unfilem1  9371  fodomfir  9396  fiin  9491  brwdomi  9637  canthwdom  9648  brwdom3i  9652  unxpwdom  9658  scott0  9955  acni  10114  djuinf  10258  pwdjudom  10284  fin1ai  10362  fin2i  10364  fin4i  10367  ssfin3ds  10399  fin23lem17  10407  fin23lem38  10418  fin23lem39  10419  isfin32i  10434  fin34  10459  isfin7-2  10465  fin1a2lem13  10481  fin12  10482  gchi  10693  wuntr  10774  wununi  10775  wunpw  10776  wunpr  10778  wun0  10787  tskpwss  10821  tskpw  10822  tsken  10823  grutr  10862  grupw  10864  grupr  10866  gruurn  10867  ingru  10884  indpi  10976  eliooord  13466  fzrev3i  13651  elfzole1  13724  elfzolt2  13725  bcp1nk  14366  rere  15171  nn0abscl  15361  climcl  15545  rlimcl  15549  rlimdm  15597  o1res  15606  rlimdmo1  15664  climcau  15719  caucvgb  15728  fprodcnv  16031  cshws0  17149  restsspw  17491  mreiincl  17654  catidex  17732  catcocl  17743  catass  17744  homa1  18104  homahom2  18105  odulat  18505  dlatjmdi  18596  psrel  18639  psref2  18640  pstr2  18641  reldir  18669  dirdm  18670  dirref  18671  dirtr  18672  dirge  18673  mgmcl  18681  submgmss  18743  submgmcl  18745  submgmmgm  18746  submss  18844  subm0cl  18846  submcl  18847  submmnd  18848  efmndbasf  18910  subgsubm  19188  symgbasf1o  19416  symginv  19444  psgneu  19548  odmulg  19598  frgpnabl  19917  dprdgrp  20049  dprdf  20050  abvfge0  20837  abveq0  20841  abvmul  20844  abvtri  20845  lbsss  21099  lbssp  21101  lbsind  21102  domnchr  21570  cssi  21725  linds1  21853  linds2  21854  lindsind  21860  opsrtoslem2  22103  opsrso  22105  mdetunilem9  22647  uniopn  22924  iunopn  22925  inopn  22926  fiinopn  22928  eltpsg  22970  eltpsgOLD  22971  basis1  22978  basis2  22979  eltg4i  22988  lmff  23330  t1sep2  23398  cmpfii  23438  ptfinfin  23548  kqhmph  23848  fbasne0  23859  0nelfb  23860  fbsspw  23861  fbasssin  23865  ufli  23943  uffixfr  23952  elfm  23976  fclsopni  24044  fclselbas  24045  ustssxp  24234  ustbasel  24236  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ustfilxp  24242  ustbas2  24255  ustbas  24257  psmetf  24337  psmet0  24339  psmettri2  24340  metflem  24359  xmetf  24360  xmeteq0  24369  xmettri2  24371  tmsxms  24520  tmsms  24521  metustsym  24589  tngnrg  24716  cncff  24938  cncfi  24939  cfili  25321  iscmet3lem2  25345  mbfres  25698  mbfimaopnlem  25709  limcresi  25940  dvcnp2  25975  dvcnp2OLD  25976  ulmcl  26442  ulmf  26443  ulmcau  26456  pserulm  26483  pserdvlem2  26490  sinq34lt0t  26569  logtayl  26720  dchrmhm  27303  lgsdir2lem2  27388  2sqlem9  27489  mulog2sum  27599  eleei  28930  uhgrf  29097  ushgrf  29098  upgrf  29121  umgrf  29133  uspgrf  29189  usgrf  29190  usgrfs  29192  nbcplgr  29469  clwlkcompim  29816  tncp  30510  eulplig  30517  grpofo  30531  grpolidinv  30533  grpoass  30535  nvvop  30641  phpar  30856  pjch1  31702  fzne1  32793  toslub  32946  tosglb  32948  chnub  32984  orngsqr  33299  fldextsubrg  33664  fldextress  33665  zhmnrg  33913  issgon  34087  measfrge0  34167  measvnul  34170  measvun  34173  fzssfzo  34516  bnj916  34909  bnj983  34927  cplgredgex  35088  acycgrcycl  35115  mfsdisj  35518  mtyf2  35519  maxsta  35522  mvtinf  35523  r1peuqusdeg1  35611  hfun  36142  hfsn  36143  hfelhf  36145  hfuni  36148  hfpw  36149  fneuni  36313  curryset  36912  mptsnunlem  37304  heibor1lem  37769  heiborlem1  37771  heiborlem3  37773  opidonOLD  37812  isexid2  37815  elrelsrelim  38444  eqvrelqsel  38572  elpcliN  39850  lnrfg  43076  sdomne0  43375  sdomne0d  43376  pwinfi2  43524  frege55lem1c  43878  gneispacef  44097  gneispacef2  44098  gneispacern2  44101  gneispace0nelrn  44102  gneispaceel  44105  gneispacess  44107  mnuop123d  44231  trintALTVD  44851  trintALT  44852  eliuniin  45001  eliuniin2  45022  disjrnmpt2  45095  fvelima2  45169  stoweidlem35  45956  saluncl  46238  saldifcl  46240  0sal  46241  sge0resplit  46327  omedm  46420  funressneu  46962  afvelrnb0  47079  afvelima  47082  rlimdmafv  47092  funressndmafv2rn  47138  rlimdmafv2  47173  elsetpreimafv  47259  oexpnegALTV  47551  gricbri  47769  grlimprop2  47810  grilcbri  47826  asslawass  47916  linindsi  48176