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  3686  elab3g  3687  elimhyp  4595  elimhyp2v  4596  elimhyp3v  4597  elimhyp4v  4598  elpwi  4611  elsni  4647  elpri  4653  eltpi  4692  snssi  4812  prssi  4825  snelpwi  5453  prelpwi  5457  elxpi  5710  releldmb  5959  relelrnb  5960  elrnmpt2d  5979  eloni  6395  limuni2  6447  funeu  6592  fneu  6678  fvelima  6973  fvelimad  6975  eloprabi  8086  fo2ndf  8144  orderseqlem  8180  tfrlem9  8423  oeeulem  8637  elqsi  8808  qsel  8834  ecopovsym  8857  elpmi  8884  elmapi  8887  pmsspw  8915  brdomi  8997  brdomiOLD  8998  en0  9056  en0r  9058  en1  9062  undomOLD  9098  mapdom1  9180  rexdif1en  9196  ominf  9291  ominfOLD  9292  unblem2  9326  unfilem1  9340  fodomfir  9365  fiin  9459  brwdomi  9605  canthwdom  9616  brwdom3i  9620  unxpwdom  9626  scott0  9923  acni  10082  djuinf  10226  pwdjudom  10252  fin1ai  10330  fin2i  10332  fin4i  10335  ssfin3ds  10367  fin23lem17  10375  fin23lem38  10386  fin23lem39  10387  isfin32i  10402  fin34  10427  isfin7-2  10433  fin1a2lem13  10449  fin12  10450  gchi  10661  wuntr  10742  wununi  10743  wunpw  10744  wunpr  10746  wun0  10755  tskpwss  10789  tskpw  10790  tsken  10791  grutr  10830  grupw  10832  grupr  10834  gruurn  10835  ingru  10852  indpi  10944  eliooord  13442  fzrev3i  13627  fzne1  13640  elfzole1  13703  elfzolt2  13704  bcp1nk  14352  rere  15157  nn0abscl  15347  climcl  15531  rlimcl  15535  rlimdm  15583  o1res  15592  rlimdmo1  15650  climcau  15703  caucvgb  15712  fprodcnv  16015  cshws0  17135  restsspw  17477  mreiincl  17640  catidex  17718  catcocl  17729  catass  17730  homa1  18090  homahom2  18091  odulat  18492  dlatjmdi  18583  psrel  18626  psref2  18627  pstr2  18628  reldir  18656  dirdm  18657  dirref  18658  dirtr  18659  dirge  18660  mgmcl  18668  submgmss  18730  submgmcl  18732  submgmmgm  18733  submss  18834  subm0cl  18836  submcl  18837  submmnd  18838  efmndbasf  18900  subgsubm  19178  symgbasf1o  19406  symginv  19434  psgneu  19538  odmulg  19588  frgpnabl  19907  dprdgrp  20039  dprdf  20040  abvfge0  20831  abveq0  20835  abvmul  20838  abvtri  20839  lbsss  21093  lbssp  21095  lbsind  21096  domnchr  21564  cssi  21719  linds1  21847  linds2  21848  lindsind  21854  opsrtoslem2  22097  opsrso  22099  mdetunilem9  22641  uniopn  22918  iunopn  22919  inopn  22920  fiinopn  22922  eltpsg  22964  eltpsgOLD  22965  basis1  22972  basis2  22973  eltg4i  22982  lmff  23324  t1sep2  23392  cmpfii  23432  ptfinfin  23542  kqhmph  23842  fbasne0  23853  0nelfb  23854  fbsspw  23855  fbasssin  23859  ufli  23937  uffixfr  23946  elfm  23970  fclsopni  24038  fclselbas  24039  ustssxp  24228  ustbasel  24230  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ustfilxp  24236  ustbas2  24249  ustbas  24251  psmetf  24331  psmet0  24333  psmettri2  24334  metflem  24353  xmetf  24354  xmeteq0  24363  xmettri2  24365  tmsxms  24514  tmsms  24515  metustsym  24583  tngnrg  24710  cncff  24932  cncfi  24933  cfili  25315  iscmet3lem2  25339  mbfres  25692  mbfimaopnlem  25703  limcresi  25934  dvcnp2  25969  dvcnp2OLD  25970  ulmcl  26438  ulmf  26439  ulmcau  26452  pserulm  26479  pserdvlem2  26486  sinq34lt0t  26565  logtayl  26716  dchrmhm  27299  lgsdir2lem2  27384  2sqlem9  27485  mulog2sum  27595  eleei  28926  uhgrf  29093  ushgrf  29094  upgrf  29117  umgrf  29129  uspgrf  29185  usgrf  29186  usgrfs  29188  nbcplgr  29465  clwlkcompim  29812  tncp  30506  eulplig  30513  grpofo  30527  grpolidinv  30529  grpoass  30531  nvvop  30637  phpar  30852  pjch1  31698  toslub  32947  tosglb  32949  chnub  32985  orngsqr  33313  fldextsubrg  33678  fldextress  33679  zhmnrg  33927  issgon  34103  measfrge0  34183  measvnul  34186  measvun  34189  fzssfzo  34532  bnj916  34925  bnj983  34943  cplgredgex  35104  acycgrcycl  35131  mfsdisj  35534  mtyf2  35535  maxsta  35538  mvtinf  35539  r1peuqusdeg1  35627  hfun  36159  hfsn  36160  hfelhf  36162  hfuni  36165  hfpw  36166  fneuni  36329  curryset  36928  mptsnunlem  37320  heibor1lem  37795  heiborlem1  37797  heiborlem3  37799  opidonOLD  37838  isexid2  37841  elrelsrelim  38469  eqvrelqsel  38597  elpcliN  39875  lnrfg  43107  sdomne0  43402  sdomne0d  43403  pwinfi2  43551  frege55lem1c  43905  gneispacef  44124  gneispacef2  44125  gneispacern2  44128  gneispace0nelrn  44129  gneispaceel  44132  gneispacess  44134  mnuop123d  44257  trintALTVD  44877  trintALT  44878  eliuniin  45038  eliuniin2  45059  disjrnmpt2  45130  fvelima2  45204  stoweidlem35  45990  saluncl  46272  saldifcl  46274  0sal  46275  sge0resplit  46361  omedm  46454  funressneu  46996  afvelrnb0  47113  afvelima  47116  rlimdmafv  47126  funressndmafv2rn  47172  rlimdmafv2  47207  elsetpreimafv  47309  oexpnegALTV  47601  gricbri  47822  grlimprop2  47888  grilcbri  47904  asslawass  48036  linindsi  48292