Theorem ibi 268

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 233	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  ibir  269  elab3gf  3629  elab3g  3630  elimhyp  4527  elimhyp2v  4528  elimhyp3v  4529  elimhyp4v  4530  elpwi  4543  elsni  4579  elpri  4586  eltpi  4627  snssi  4724  prssi  4759  snelpwi  5390  prelpwi  5393  elxpi  5647  releldmb  5895  relelrnb  5896  elrnmpt2d  5915  eloni  6327  limuni2  6380  funeu  6517  fneu  6602  fvelima2  6886  fvelima  6899  fvelimad  6901  eloprabi  8012  fo2ndf  8067  orderseqlem  8104  tfrlem9  8321  oeeulem  8534  elqsi  8709  qsel  8740  ecopovsym  8763  elpmi  8790  elmapi  8793  pmsspw  8822  brdomi  8903  en0  8962  en0r  8964  en1  8968  mapdom1  9077  rexdif1en  9092  ominf  9171  unblem2  9200  unfilem1  9212  fodomfir  9235  fiin  9332  brwdomi  9480  canthwdom  9491  brwdom3i  9495  unxpwdom  9501  scott0  9808  acni  9965  djuinf  10109  pwdjudom  10135  fin1ai  10213  fin2i  10215  fin4i  10218  ssfin3ds  10250  fin23lem17  10258  fin23lem38  10269  fin23lem39  10270  isfin32i  10285  fin34  10310  isfin7-2  10316  fin1a2lem13  10332  fin12  10333  gchi  10545  wuntr  10626  wununi  10627  wunpw  10628  wunpr  10630  wun0  10639  tskpwss  10673  tskpw  10674  tsken  10675  grutr  10714  grupw  10716  grupr  10718  gruurn  10719  ingru  10736  indpi  10828  eliooord  13356  fzrev3i  13543  fzne1  13556  elfzole1  13620  elfzolt2  13621  bcp1nk  14277  rere  15082  nn0abscl  15272  climcl  15459  rlimcl  15463  rlimdm  15511  o1res  15520  rlimdmo1  15578  climcau  15631  caucvgb  15640  fprodcnv  15946  cshws0  17070  restsspw  17392  mreiincl  17556  catidex  17638  catcocl  17649  catass  17650  homa1  18002  homahom2  18003  odulat  18399  dlatjmdi  18490  psrel  18533  psref2  18534  pstr2  18535  reldir  18563  dirdm  18564  dirref  18565  dirtr  18566  dirge  18567  chnub  18586  mgmcl  18609  submgmss  18671  submgmcl  18673  submgmmgm  18674  submss  18775  subm0cl  18777  submcl  18778  submmnd  18779  efmndbasf  18841  subgsubm  19122  symgbasf1o  19348  symginv  19375  psgneu  19479  odmulg  19529  frgpnabl  19848  dprdgrp  19980  dprdf  19981  abvfge0  20793  abveq0  20797  abvmul  20800  abvtri  20801  orngsqr  20845  lbsss  21074  lbssp  21076  lbsind  21077  domnchr  21514  cssi  21666  linds1  21792  linds2  21793  lindsind  21799  opsrtoslem2  22039  opsrso  22041  mdetunilem9  22610  uniopn  22887  iunopn  22888  inopn  22889  fiinopn  22891  eltpsg  22933  basis1  22940  basis2  22941  eltg4i  22950  lmff  23291  t1sep2  23359  cmpfii  23399  ptfinfin  23509  kqhmph  23809  fbasne0  23820  0nelfb  23821  fbsspw  23822  fbasssin  23826  ufli  23904  uffixfr  23913  elfm  23937  fclsopni  24005  fclselbas  24006  ustssxp  24195  ustbasel  24197  ustincl  24198  ustdiag  24199  ustinvel  24200  ustexhalf  24201  ustfilxp  24203  ustbas2  24215  ustbas  24217  psmetf  24296  psmet0  24298  psmettri2  24299  metflem  24318  xmetf  24319  xmeteq0  24328  xmettri2  24330  tmsxms  24476  tmsms  24477  metustsym  24545  tngnrg  24664  cncff  24885  cncfi  24886  cfili  25260  iscmet3lem2  25284  mbfres  25636  mbfimaopnlem  25647  limcresi  25877  dvcnp2  25912  ulmcl  26371  ulmf  26372  ulmcau  26385  pserulm  26412  pserdvlem2  26418  sinq34lt0t  26498  logtayl  26649  dchrmhm  27229  lgsdir2lem2  27314  2sqlem9  27415  mulog2sum  27525  newbdayim  27920  eleei  28991  uhgrf  29156  ushgrf  29157  upgrf  29180  umgrf  29192  uspgrf  29248  usgrf  29249  usgrfs  29251  nbcplgr  29528  clwlkcompim  29873  tncp  30574  eulplig  30581  grpofo  30595  grpolidinv  30597  grpoass  30599  nvvop  30705  phpar  30920  pjch1  31766  nn0mnfxrd  32850  toslub  33059  tosglb  33061  suppgsumssiun  33160  exsslsb  33788  fldextsubrg  33840  fldextress  33842  zhmnrg  34156  issgon  34314  measfrge0  34394  measvnul  34397  measvun  34400  fzssfzo  34730  bnj916  35122  bnj983  35140  cplgredgex  35356  acycgrcycl  35382  mfsdisj  35785  mtyf2  35786  maxsta  35789  mvtinf  35790  r1peuqusdeg1  35878  hfun  36413  hfsn  36414  hfelhf  36416  hfuni  36419  hfpw  36420  fneuni  36582  elttcirr  36766  curryset  37306  mptsnunlem  37707  heibor1lem  38183  heiborlem1  38185  heiborlem3  38187  opidonOLD  38226  isexid2  38229  elrelsrelim  38817  presucmap  38869  eqvrelqsel  39074  eldisjsim1  39308  elpcliN  40392  lnrfg  43571  sdomne0  43864  sdomne0d  43865  pwinfi2  44013  frege55lem1c  44367  gneispacef  44586  gneispacef2  44587  gneispacern2  44590  gneispace0nelrn  44591  gneispaceel  44594  gneispacess  44596  mnuop123d  44713  trintALTVD  45330  trintALT  45331  eliuniin  45553  eliuniin2  45574  disjrnmpt2  45642  stoweidlem35  46485  saluncl  46767  saldifcl  46769  0sal  46770  sge0resplit  46856  omedm  46949  funressneu  47517  afvelrnb0  47634  afvelima  47637  rlimdmafv  47647  funressndmafv2rn  47693  rlimdmafv2  47728  elsetpreimafv  47867  oexpnegALTV  48175  gricbri  48414  grlimprop2  48484  grilcbri  48507  asslawass  48691  linindsi  48945  inisegn0a  49333  eloprab1st2nd  49365  uobrcl  49690  uobeq2  49898  isinito2  49996  basrestermcfolem  50068  discsnterm  50071  islmd  50162