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  3641  elab3g  3642  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elpwi  4563  elsni  4599  elpri  4606  eltpi  4647  snssi  4766  prssi  4779  snelpwi  5399  prelpwi  5402  elxpi  5654  releldmb  5903  relelrnb  5904  elrnmpt2d  5923  eloni  6335  limuni2  6388  funeu  6525  fneu  6610  fvelima2  6894  fvelima  6907  fvelimad  6909  eloprabi  8017  fo2ndf  8073  orderseqlem  8109  tfrlem9  8326  oeeulem  8539  elqsi  8714  qsel  8745  ecopovsym  8768  elpmi  8795  elmapi  8798  pmsspw  8827  brdomi  8908  en0  8967  en0r  8969  en1  8973  mapdom1  9082  rexdif1en  9097  ominf  9176  unblem2  9205  unfilem1  9217  fodomfir  9240  fiin  9337  brwdomi  9485  canthwdom  9496  brwdom3i  9500  unxpwdom  9506  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  13333  fzrev3i  13519  fzne1  13532  elfzole1  13595  elfzolt2  13596  bcp1nk  14252  rere  15057  nn0abscl  15247  climcl  15434  rlimcl  15438  rlimdm  15486  o1res  15495  rlimdmo1  15553  climcau  15606  caucvgb  15615  fprodcnv  15918  cshws0  17041  restsspw  17363  mreiincl  17527  catidex  17609  catcocl  17620  catass  17621  homa1  17973  homahom2  17974  odulat  18370  dlatjmdi  18461  psrel  18504  psref2  18505  pstr2  18506  reldir  18534  dirdm  18535  dirref  18536  dirtr  18537  dirge  18538  chnub  18557  mgmcl  18580  submgmss  18642  submgmcl  18644  submgmmgm  18645  submss  18746  subm0cl  18748  submcl  18749  submmnd  18750  efmndbasf  18812  subgsubm  19090  symgbasf1o  19316  symginv  19343  psgneu  19447  odmulg  19497  frgpnabl  19816  dprdgrp  19948  dprdf  19949  abvfge0  20759  abveq0  20763  abvmul  20766  abvtri  20767  orngsqr  20811  lbsss  21041  lbssp  21043  lbsind  21044  domnchr  21499  cssi  21651  linds1  21777  linds2  21778  lindsind  21784  opsrtoslem2  22023  opsrso  22025  mdetunilem9  22576  uniopn  22853  iunopn  22854  inopn  22855  fiinopn  22857  eltpsg  22899  basis1  22906  basis2  22907  eltg4i  22916  lmff  23257  t1sep2  23325  cmpfii  23365  ptfinfin  23475  kqhmph  23775  fbasne0  23786  0nelfb  23787  fbsspw  23788  fbasssin  23792  ufli  23870  uffixfr  23879  elfm  23903  fclsopni  23971  fclselbas  23972  ustssxp  24161  ustbasel  24163  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ustfilxp  24169  ustbas2  24181  ustbas  24183  psmetf  24262  psmet0  24264  psmettri2  24265  metflem  24284  xmetf  24285  xmeteq0  24294  xmettri2  24296  tmsxms  24442  tmsms  24443  metustsym  24511  tngnrg  24630  cncff  24854  cncfi  24855  cfili  25236  iscmet3lem2  25260  mbfres  25613  mbfimaopnlem  25624  limcresi  25854  dvcnp2  25889  dvcnp2OLD  25890  ulmcl  26358  ulmf  26359  ulmcau  26372  pserulm  26399  pserdvlem2  26406  sinq34lt0t  26486  logtayl  26637  dchrmhm  27220  lgsdir2lem2  27305  2sqlem9  27406  mulog2sum  27516  newbdayim  27911  eleei  28982  uhgrf  29147  ushgrf  29148  upgrf  29171  umgrf  29183  uspgrf  29239  usgrf  29240  usgrfs  29242  nbcplgr  29519  clwlkcompim  29865  tncp  30565  eulplig  30572  grpofo  30586  grpolidinv  30588  grpoass  30590  nvvop  30696  phpar  30911  pjch1  31757  nn0mnfxrd  32841  toslub  33065  tosglb  33067  suppgsumssiun  33165  exsslsb  33773  fldextsubrg  33826  fldextress  33828  zhmnrg  34142  issgon  34300  measfrge0  34380  measvnul  34383  measvun  34386  fzssfzo  34716  bnj916  35108  bnj983  35126  cplgredgex  35334  acycgrcycl  35360  mfsdisj  35763  mtyf2  35764  maxsta  35767  mvtinf  35768  r1peuqusdeg1  35856  hfun  36391  hfsn  36392  hfelhf  36394  hfuni  36397  hfpw  36398  fneuni  36560  curryset  37191  mptsnunlem  37590  heibor1lem  38057  heiborlem1  38059  heiborlem3  38061  opidonOLD  38100  isexid2  38103  elrelsrelim  38691  presucmap  38743  eqvrelqsel  38948  eldisjsim1  39182  elpcliN  40266  lnrfg  43473  sdomne0  43766  sdomne0d  43767  pwinfi2  43915  frege55lem1c  44269  gneispacef  44488  gneispacef2  44489  gneispacern2  44492  gneispace0nelrn  44493  gneispaceel  44496  gneispacess  44498  mnuop123d  44615  trintALTVD  45232  trintALT  45233  eliuniin  45455  eliuniin2  45476  disjrnmpt2  45544  stoweidlem35  46390  saluncl  46672  saldifcl  46674  0sal  46675  sge0resplit  46761  omedm  46854  funressneu  47404  afvelrnb0  47521  afvelima  47524  rlimdmafv  47534  funressndmafv2rn  47580  rlimdmafv2  47615  elsetpreimafv  47742  oexpnegALTV  48034  gricbri  48273  grlimprop2  48343  grilcbri  48366  asslawass  48550  linindsi  48804  inisegn0a  49192  eloprab1st2nd  49224  uobrcl  49549  uobeq2  49757  isinito2  49855  basrestermcfolem  49927  discsnterm  49930  islmd  50021