Theorem ibi 266

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ibir  267  elab3gf  3616  elab3g  3617  elimhyp  4525  elimhyp2v  4526  elimhyp3v  4527  elimhyp4v  4528  elpwi  4543  elsni  4579  elpri  4584  eltpi  4624  snssi  4742  prssi  4755  prelpwi  5364  elxpi  5612  releldmb  5858  relelrnb  5859  elrnmpt2d  5875  eloni  6280  limuni2  6331  funeu  6466  fneu  6552  fvelima  6844  fvelimad  6845  eloprabi  7912  fo2ndf  7971  tfrlem9  8225  oeeulem  8441  elqsi  8568  qsel  8594  ecopovsym  8617  elpmi  8643  elmapi  8646  pmsspw  8674  brdomi  8757  brdomiOLD  8758  en0  8812  en0r  8815  en1  8820  undomOLD  8856  mapdom1  8938  ominf  9044  unblem2  9076  unfilem1  9087  fiin  9190  brwdomi  9336  canthwdom  9347  brwdom3i  9351  unxpwdom  9357  scott0  9653  acni  9810  djuinf  9953  pwdjudom  9981  fin1ai  10058  fin2i  10060  fin4i  10063  ssfin3ds  10095  fin23lem17  10103  fin23lem38  10114  fin23lem39  10115  isfin32i  10130  fin34  10155  isfin7-2  10161  fin1a2lem13  10177  fin12  10178  gchi  10389  wuntr  10470  wununi  10471  wunpw  10472  wunpr  10474  wun0  10483  tskpwss  10517  tskpw  10518  tsken  10519  grutr  10558  grupw  10560  grupr  10562  gruurn  10563  ingru  10580  indpi  10672  eliooord  13147  fzrev3i  13332  elfzole1  13404  elfzolt2  13405  bcp1nk  14040  rere  14842  nn0abscl  15033  climcl  15217  rlimcl  15221  rlimdm  15269  o1res  15278  rlimdmo1  15336  climcau  15391  caucvgb  15400  fprodcnv  15702  cshws0  16812  restsspw  17151  mreiincl  17314  catidex  17392  catcocl  17403  catass  17404  homa1  17761  homahom2  17762  odulat  18162  dlatjmdi  18253  psrel  18296  psref2  18297  pstr2  18298  reldir  18326  dirdm  18327  dirref  18328  dirtr  18329  dirge  18330  mgmcl  18338  submss  18457  subm0cl  18459  submcl  18460  submmnd  18461  efmndbasf  18523  subgsubm  18786  symgbasf1o  18991  symginv  19019  psgneu  19123  odmulg  19172  frgpnabl  19485  dprdgrp  19617  dprdf  19618  abvfge0  20091  abveq0  20095  abvmul  20098  abvtri  20099  lbsss  20348  lbssp  20350  lbsind  20351  domnchr  20745  cssi  20898  linds1  21026  linds2  21027  lindsind  21033  opsrtoslem2  21272  opsrso  21274  mdetunilem9  21778  uniopn  22055  iunopn  22056  inopn  22057  fiinopn  22059  eltpsg  22101  eltpsgOLD  22102  basis1  22109  basis2  22110  eltg4i  22119  lmff  22461  t1sep2  22529  cmpfii  22569  ptfinfin  22679  kqhmph  22979  fbasne0  22990  0nelfb  22991  fbsspw  22992  fbasssin  22996  ufli  23074  uffixfr  23083  elfm  23107  fclsopni  23175  fclselbas  23176  ustssxp  23365  ustbasel  23367  ustincl  23368  ustdiag  23369  ustinvel  23370  ustexhalf  23371  ustfilxp  23373  ustbas2  23386  ustbas  23388  psmetf  23468  psmet0  23470  psmettri2  23471  metflem  23490  xmetf  23491  xmeteq0  23500  xmettri2  23502  tmsxms  23651  tmsms  23652  metustsym  23720  tngnrg  23847  cncff  24065  cncfi  24066  cfili  24441  iscmet3lem2  24465  mbfres  24817  mbfimaopnlem  24828  limcresi  25058  dvcnp2  25093  ulmcl  25549  ulmf  25550  ulmcau  25563  pserulm  25590  pserdvlem2  25596  sinq34lt0t  25675  logtayl  25824  dchrmhm  26398  lgsdir2lem2  26483  2sqlem9  26584  mulog2sum  26694  eleei  27274  uhgrf  27441  ushgrf  27442  upgrf  27465  umgrf  27477  uspgrf  27533  usgrf  27534  usgrfs  27536  nbcplgr  27810  clwlkcompim  28157  tncp  28849  eulplig  28856  grpofo  28870  grpolidinv  28872  grpoass  28874  nvvop  28980  phpar  29195  pjch1  30041  fzne1  31118  toslub  31260  tosglb  31262  orngsqr  31512  fldextsubrg  31735  fldextress  31736  zhmnrg  31926  issgon  32100  measfrge0  32180  measvnul  32183  measvun  32186  fzssfzo  32527  bnj916  32922  bnj983  32940  cplgredgex  33091  acycgrcycl  33118  mfsdisj  33521  mtyf2  33522  maxsta  33525  mvtinf  33526  orderseqlem  33810  hfun  34489  hfsn  34490  hfelhf  34492  hfuni  34495  hfpw  34496  fneuni  34545  curryset  35144  mptsnunlem  35518  heibor1lem  35976  heiborlem1  35978  heiborlem3  35980  opidonOLD  36019  isexid2  36022  elrelsrelim  36613  eqvrelqsel  36736  elpcliN  37914  lnrfg  40951  pwinfi2  41176  frege55lem1c  41531  gneispacef  41752  gneispacef2  41753  gneispacern2  41756  gneispace0nelrn  41757  gneispaceel  41760  gneispacess  41762  mnuop123d  41887  trintALTVD  42507  trintALT  42508  eliuniin  42656  eliuniin2  42676  disjrnmpt2  42733  fvelima2  42813  stoweidlem35  43583  saluncl  43865  saldifcl  43867  0sal  43868  sge0resplit  43951  omedm  44044  funressneu  44552  afvelrnb0  44667  afvelima  44670  rlimdmafv  44680  funressndmafv2rn  44726  rlimdmafv2  44761  elsetpreimafv  44848  oexpnegALTV  45140  isisomgr  45287  submgmss  45357  submgmcl  45359  submgmmgm  45360  asslawass  45398  linindsi  45799