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  3639  elab3g  3640  elimhyp  4556  elimhyp2v  4557  elimhyp3v  4558  elimhyp4v  4559  elpwi  4572  elsni  4608  elpri  4613  eltpi  4653  snssi  4773  prssi  4786  snelpwi  5405  prelpwi  5409  elxpi  5660  releldmb  5906  relelrnb  5907  elrnmpt2d  5923  eloni  6332  limuni2  6384  funeu  6531  fneu  6617  fvelima  6913  fvelimad  6914  eloprabi  8000  fo2ndf  8058  orderseqlem  8094  tfrlem9  8336  oeeulem  8553  elqsi  8716  qsel  8742  ecopovsym  8765  elpmi  8791  elmapi  8794  pmsspw  8822  brdomi  8905  brdomiOLD  8906  en0  8964  en0r  8967  en1  8972  undomOLD  9011  mapdom1  9093  rexdif1en  9109  ominf  9209  ominfOLD  9210  unblem2  9247  unfilem1  9261  fiin  9367  brwdomi  9513  canthwdom  9524  brwdom3i  9528  unxpwdom  9534  scott0  9831  acni  9990  djuinf  10133  pwdjudom  10161  fin1ai  10238  fin2i  10240  fin4i  10243  ssfin3ds  10275  fin23lem17  10283  fin23lem38  10294  fin23lem39  10295  isfin32i  10310  fin34  10335  isfin7-2  10341  fin1a2lem13  10357  fin12  10358  gchi  10569  wuntr  10650  wununi  10651  wunpw  10652  wunpr  10654  wun0  10663  tskpwss  10697  tskpw  10698  tsken  10699  grutr  10738  grupw  10740  grupr  10742  gruurn  10743  ingru  10760  indpi  10852  eliooord  13333  fzrev3i  13518  elfzole1  13590  elfzolt2  13591  bcp1nk  14227  rere  15019  nn0abscl  15209  climcl  15393  rlimcl  15397  rlimdm  15445  o1res  15454  rlimdmo1  15512  climcau  15567  caucvgb  15576  fprodcnv  15877  cshws0  16985  restsspw  17327  mreiincl  17490  catidex  17568  catcocl  17579  catass  17580  homa1  17937  homahom2  17938  odulat  18338  dlatjmdi  18429  psrel  18472  psref2  18473  pstr2  18474  reldir  18502  dirdm  18503  dirref  18504  dirtr  18505  dirge  18506  mgmcl  18514  submss  18634  subm0cl  18636  submcl  18637  submmnd  18638  efmndbasf  18699  subgsubm  18964  symgbasf1o  19170  symginv  19198  psgneu  19302  odmulg  19352  frgpnabl  19667  dprdgrp  19798  dprdf  19799  abvfge0  20337  abveq0  20341  abvmul  20344  abvtri  20345  lbsss  20595  lbssp  20597  lbsind  20598  domnchr  20972  cssi  21125  linds1  21253  linds2  21254  lindsind  21260  opsrtoslem2  21500  opsrso  21502  mdetunilem9  22006  uniopn  22283  iunopn  22284  inopn  22285  fiinopn  22287  eltpsg  22329  eltpsgOLD  22330  basis1  22337  basis2  22338  eltg4i  22347  lmff  22689  t1sep2  22757  cmpfii  22797  ptfinfin  22907  kqhmph  23207  fbasne0  23218  0nelfb  23219  fbsspw  23220  fbasssin  23224  ufli  23302  uffixfr  23311  elfm  23335  fclsopni  23403  fclselbas  23404  ustssxp  23593  ustbasel  23595  ustincl  23596  ustdiag  23597  ustinvel  23598  ustexhalf  23599  ustfilxp  23601  ustbas2  23614  ustbas  23616  psmetf  23696  psmet0  23698  psmettri2  23699  metflem  23718  xmetf  23719  xmeteq0  23728  xmettri2  23730  tmsxms  23879  tmsms  23880  metustsym  23948  tngnrg  24075  cncff  24293  cncfi  24294  cfili  24669  iscmet3lem2  24693  mbfres  25045  mbfimaopnlem  25056  limcresi  25286  dvcnp2  25321  ulmcl  25777  ulmf  25778  ulmcau  25791  pserulm  25818  pserdvlem2  25824  sinq34lt0t  25903  logtayl  26052  dchrmhm  26626  lgsdir2lem2  26711  2sqlem9  26812  mulog2sum  26922  eleei  27909  uhgrf  28076  ushgrf  28077  upgrf  28100  umgrf  28112  uspgrf  28168  usgrf  28169  usgrfs  28171  nbcplgr  28445  clwlkcompim  28791  tncp  29483  eulplig  29490  grpofo  29504  grpolidinv  29506  grpoass  29508  nvvop  29614  phpar  29829  pjch1  30675  fzne1  31759  toslub  31903  tosglb  31905  orngsqr  32170  fldextsubrg  32427  fldextress  32428  zhmnrg  32637  issgon  32811  measfrge0  32891  measvnul  32894  measvun  32897  fzssfzo  33240  bnj916  33634  bnj983  33652  cplgredgex  33801  acycgrcycl  33828  mfsdisj  34231  mtyf2  34232  maxsta  34235  mvtinf  34236  hfun  34839  hfsn  34840  hfelhf  34842  hfuni  34845  hfpw  34846  fneuni  34895  curryset  35490  mptsnunlem  35882  heibor1lem  36341  heiborlem1  36343  heiborlem3  36345  opidonOLD  36384  isexid2  36387  elrelsrelim  37023  eqvrelqsel  37151  elpcliN  38429  lnrfg  41504  sdomne0  41807  sdomne0d  41808  pwinfi2  41956  frege55lem1c  42310  gneispacef  42529  gneispacef2  42530  gneispacern2  42533  gneispace0nelrn  42534  gneispaceel  42537  gneispacess  42539  mnuop123d  42664  trintALTVD  43284  trintALT  43285  eliuniin  43431  eliuniin2  43452  disjrnmpt2  43529  fvelima2  43609  stoweidlem35  44396  saluncl  44678  saldifcl  44680  0sal  44681  sge0resplit  44767  omedm  44860  funressneu  45401  afvelrnb0  45516  afvelima  45519  rlimdmafv  45529  funressndmafv2rn  45575  rlimdmafv2  45610  elsetpreimafv  45697  oexpnegALTV  45989  isisomgr  46136  submgmss  46206  submgmcl  46208  submgmmgm  46209  asslawass  46247  linindsi  46648