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  3640  elab3g  3641  elimhyp  4541  elimhyp2v  4542  elimhyp3v  4543  elimhyp4v  4544  elpwi  4557  elsni  4593  elpri  4600  eltpi  4641  snssi  4760  prssi  4773  snelpwi  5385  prelpwi  5388  elxpi  5638  releldmb  5886  relelrnb  5887  elrnmpt2d  5906  eloni  6316  limuni2  6369  funeu  6506  fneu  6591  fvelima2  6874  fvelima  6887  fvelimad  6889  eloprabi  7995  fo2ndf  8051  orderseqlem  8087  tfrlem9  8304  oeeulem  8516  elqsi  8690  qsel  8720  ecopovsym  8743  elpmi  8770  elmapi  8773  pmsspw  8801  brdomi  8882  en0  8940  en0r  8942  en1  8946  mapdom1  9055  rexdif1en  9070  ominf  9148  unblem2  9177  unfilem1  9189  fodomfir  9212  fiin  9306  brwdomi  9454  canthwdom  9465  brwdom3i  9469  unxpwdom  9475  scott0  9779  acni  9936  djuinf  10080  pwdjudom  10106  fin1ai  10184  fin2i  10186  fin4i  10189  ssfin3ds  10221  fin23lem17  10229  fin23lem38  10240  fin23lem39  10241  isfin32i  10256  fin34  10281  isfin7-2  10287  fin1a2lem13  10303  fin12  10304  gchi  10515  wuntr  10596  wununi  10597  wunpw  10598  wunpr  10600  wun0  10609  tskpwss  10643  tskpw  10644  tsken  10645  grutr  10684  grupw  10686  grupr  10688  gruurn  10689  ingru  10706  indpi  10798  eliooord  13305  fzrev3i  13491  fzne1  13504  elfzole1  13567  elfzolt2  13568  bcp1nk  14224  rere  15029  nn0abscl  15219  climcl  15406  rlimcl  15410  rlimdm  15458  o1res  15467  rlimdmo1  15525  climcau  15578  caucvgb  15587  fprodcnv  15890  cshws0  17013  restsspw  17335  mreiincl  17498  catidex  17580  catcocl  17591  catass  17592  homa1  17944  homahom2  17945  odulat  18341  dlatjmdi  18432  psrel  18475  psref2  18476  pstr2  18477  reldir  18505  dirdm  18506  dirref  18507  dirtr  18508  dirge  18509  chnub  18528  mgmcl  18551  submgmss  18613  submgmcl  18615  submgmmgm  18616  submss  18717  subm0cl  18719  submcl  18720  submmnd  18721  efmndbasf  18783  subgsubm  19061  symgbasf1o  19288  symginv  19315  psgneu  19419  odmulg  19469  frgpnabl  19788  dprdgrp  19920  dprdf  19921  abvfge0  20730  abveq0  20734  abvmul  20737  abvtri  20738  orngsqr  20782  lbsss  21012  lbssp  21014  lbsind  21015  domnchr  21470  cssi  21622  linds1  21748  linds2  21749  lindsind  21755  opsrtoslem2  21992  opsrso  21994  mdetunilem9  22536  uniopn  22813  iunopn  22814  inopn  22815  fiinopn  22817  eltpsg  22859  basis1  22866  basis2  22867  eltg4i  22876  lmff  23217  t1sep2  23285  cmpfii  23325  ptfinfin  23435  kqhmph  23735  fbasne0  23746  0nelfb  23747  fbsspw  23748  fbasssin  23752  ufli  23830  uffixfr  23839  elfm  23863  fclsopni  23931  fclselbas  23932  ustssxp  24121  ustbasel  24123  ustincl  24124  ustdiag  24125  ustinvel  24126  ustexhalf  24127  ustfilxp  24129  ustbas2  24141  ustbas  24143  psmetf  24222  psmet0  24224  psmettri2  24225  metflem  24244  xmetf  24245  xmeteq0  24254  xmettri2  24256  tmsxms  24402  tmsms  24403  metustsym  24471  tngnrg  24590  cncff  24814  cncfi  24815  cfili  25196  iscmet3lem2  25220  mbfres  25573  mbfimaopnlem  25584  limcresi  25814  dvcnp2  25849  dvcnp2OLD  25850  ulmcl  26318  ulmf  26319  ulmcau  26332  pserulm  26359  pserdvlem2  26366  sinq34lt0t  26446  logtayl  26597  dchrmhm  27180  lgsdir2lem2  27265  2sqlem9  27366  mulog2sum  27476  newbdayim  27849  eleei  28876  uhgrf  29041  ushgrf  29042  upgrf  29065  umgrf  29077  uspgrf  29133  usgrf  29134  usgrfs  29136  nbcplgr  29413  clwlkcompim  29759  tncp  30456  eulplig  30463  grpofo  30477  grpolidinv  30479  grpoass  30481  nvvop  30587  phpar  30802  pjch1  31648  toslub  32952  tosglb  32954  exsslsb  33607  fldextsubrg  33660  fldextress  33662  zhmnrg  33976  issgon  34134  measfrge0  34214  measvnul  34217  measvun  34220  fzssfzo  34550  bnj916  34943  bnj983  34961  cplgredgex  35163  acycgrcycl  35189  mfsdisj  35592  mtyf2  35593  maxsta  35596  mvtinf  35597  r1peuqusdeg1  35685  hfun  36218  hfsn  36219  hfelhf  36221  hfuni  36224  hfpw  36225  fneuni  36387  curryset  36986  mptsnunlem  37378  heibor1lem  37855  heiborlem1  37857  heiborlem3  37859  opidonOLD  37898  isexid2  37901  elrelsrelim  38531  eqvrelqsel  38659  elpcliN  39938  lnrfg  43158  sdomne0  43452  sdomne0d  43453  pwinfi2  43601  frege55lem1c  43955  gneispacef  44174  gneispacef2  44175  gneispacern2  44178  gneispace0nelrn  44179  gneispaceel  44182  gneispacess  44184  mnuop123d  44301  trintALTVD  44918  trintALT  44919  eliuniin  45142  eliuniin2  45163  disjrnmpt2  45231  stoweidlem35  46079  saluncl  46361  saldifcl  46363  0sal  46364  sge0resplit  46450  omedm  46543  funressneu  47084  afvelrnb0  47201  afvelima  47204  rlimdmafv  47214  funressndmafv2rn  47260  rlimdmafv2  47295  elsetpreimafv  47422  oexpnegALTV  47714  gricbri  47953  grlimprop2  48023  grilcbri  48046  asslawass  48230  linindsi  48485  inisegn0a  48873  eloprab1st2nd  48905  uobrcl  49231  uobeq2  49439  isinito2  49537  basrestermcfolem  49609  discsnterm  49612  islmd  49703