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  3627  elab3g  3628  elimhyp  4532  elimhyp2v  4533  elimhyp3v  4534  elimhyp4v  4535  elpwi  4548  elsni  4584  elpri  4591  eltpi  4632  snssi  4729  prssi  4764  snelpwi  5396  prelpwi  5399  elxpi  5653  releldmb  5901  relelrnb  5902  elrnmpt2d  5921  eloni  6333  limuni2  6386  funeu  6523  fneu  6608  fvelima2  6892  fvelima  6905  fvelimad  6907  eloprabi  8016  fo2ndf  8071  orderseqlem  8107  tfrlem9  8324  oeeulem  8537  elqsi  8712  qsel  8743  ecopovsym  8766  elpmi  8793  elmapi  8796  pmsspw  8825  brdomi  8906  en0  8965  en0r  8967  en1  8971  mapdom1  9080  rexdif1en  9095  ominf  9174  unblem2  9203  unfilem1  9215  fodomfir  9238  fiin  9335  brwdomi  9483  canthwdom  9494  brwdom3i  9498  unxpwdom  9504  scott0  9810  acni  9967  djuinf  10111  pwdjudom  10137  fin1ai  10215  fin2i  10217  fin4i  10220  ssfin3ds  10252  fin23lem17  10260  fin23lem38  10271  fin23lem39  10272  isfin32i  10287  fin34  10312  isfin7-2  10318  fin1a2lem13  10334  fin12  10335  gchi  10547  wuntr  10628  wununi  10629  wunpw  10630  wunpr  10632  wun0  10641  tskpwss  10675  tskpw  10676  tsken  10677  grutr  10716  grupw  10718  grupr  10720  gruurn  10721  ingru  10738  indpi  10830  eliooord  13358  fzrev3i  13545  fzne1  13558  elfzole1  13622  elfzolt2  13623  bcp1nk  14279  rere  15084  nn0abscl  15274  climcl  15461  rlimcl  15465  rlimdm  15513  o1res  15522  rlimdmo1  15580  climcau  15633  caucvgb  15642  fprodcnv  15948  cshws0  17072  restsspw  17394  mreiincl  17558  catidex  17640  catcocl  17651  catass  17652  homa1  18004  homahom2  18005  odulat  18401  dlatjmdi  18492  psrel  18535  psref2  18536  pstr2  18537  reldir  18565  dirdm  18566  dirref  18567  dirtr  18568  dirge  18569  chnub  18588  mgmcl  18611  submgmss  18673  submgmcl  18675  submgmmgm  18676  submss  18777  subm0cl  18779  submcl  18780  submmnd  18781  efmndbasf  18843  subgsubm  19124  symgbasf1o  19350  symginv  19377  psgneu  19481  odmulg  19531  frgpnabl  19850  dprdgrp  19982  dprdf  19983  abvfge0  20791  abveq0  20795  abvmul  20798  abvtri  20799  orngsqr  20843  lbsss  21072  lbssp  21074  lbsind  21075  domnchr  21512  cssi  21664  linds1  21790  linds2  21791  lindsind  21797  opsrtoslem2  22034  opsrso  22036  mdetunilem9  22585  uniopn  22862  iunopn  22863  inopn  22864  fiinopn  22866  eltpsg  22908  basis1  22915  basis2  22916  eltg4i  22925  lmff  23266  t1sep2  23334  cmpfii  23374  ptfinfin  23484  kqhmph  23784  fbasne0  23795  0nelfb  23796  fbsspw  23797  fbasssin  23801  ufli  23879  uffixfr  23888  elfm  23912  fclsopni  23980  fclselbas  23981  ustssxp  24170  ustbasel  24172  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ustfilxp  24178  ustbas2  24190  ustbas  24192  psmetf  24271  psmet0  24273  psmettri2  24274  metflem  24293  xmetf  24294  xmeteq0  24303  xmettri2  24305  tmsxms  24451  tmsms  24452  metustsym  24520  tngnrg  24639  cncff  24860  cncfi  24861  cfili  25235  iscmet3lem2  25259  mbfres  25611  mbfimaopnlem  25622  limcresi  25852  dvcnp2  25887  ulmcl  26346  ulmf  26347  ulmcau  26360  pserulm  26387  pserdvlem2  26393  sinq34lt0t  26473  logtayl  26624  dchrmhm  27204  lgsdir2lem2  27289  2sqlem9  27390  mulog2sum  27500  newbdayim  27895  eleei  28966  uhgrf  29131  ushgrf  29132  upgrf  29155  umgrf  29167  uspgrf  29223  usgrf  29224  usgrfs  29226  nbcplgr  29503  clwlkcompim  29848  tncp  30549  eulplig  30556  grpofo  30570  grpolidinv  30572  grpoass  30574  nvvop  30680  phpar  30895  pjch1  31741  nn0mnfxrd  32824  toslub  33033  tosglb  33035  suppgsumssiun  33133  exsslsb  33741  fldextsubrg  33793  fldextress  33795  zhmnrg  34109  issgon  34267  measfrge0  34347  measvnul  34350  measvun  34353  fzssfzo  34683  bnj916  35075  bnj983  35093  cplgredgex  35303  acycgrcycl  35329  mfsdisj  35732  mtyf2  35733  maxsta  35736  mvtinf  35737  r1peuqusdeg1  35825  hfun  36360  hfsn  36361  hfelhf  36363  hfuni  36366  hfpw  36367  fneuni  36529  elttcirr  36713  curryset  37253  mptsnunlem  37654  heibor1lem  38130  heiborlem1  38132  heiborlem3  38134  opidonOLD  38173  isexid2  38176  elrelsrelim  38764  presucmap  38816  eqvrelqsel  39021  eldisjsim1  39255  elpcliN  40339  lnrfg  43547  sdomne0  43840  sdomne0d  43841  pwinfi2  43989  frege55lem1c  44343  gneispacef  44562  gneispacef2  44563  gneispacern2  44566  gneispace0nelrn  44567  gneispaceel  44570  gneispacess  44572  mnuop123d  44689  trintALTVD  45306  trintALT  45307  eliuniin  45529  eliuniin2  45550  disjrnmpt2  45618  stoweidlem35  46463  saluncl  46745  saldifcl  46747  0sal  46748  sge0resplit  46834  omedm  46927  funressneu  47495  afvelrnb0  47612  afvelima  47615  rlimdmafv  47625  funressndmafv2rn  47671  rlimdmafv2  47706  elsetpreimafv  47845  oexpnegALTV  48153  gricbri  48392  grlimprop2  48462  grilcbri  48485  asslawass  48669  linindsi  48923  inisegn0a  49311  eloprab1st2nd  49343  uobrcl  49668  uobeq2  49876  isinito2  49974  basrestermcfolem  50046  discsnterm  50049  islmd  50140