Theorem ibi 269

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ibir  270  elab3gf  3642  elab3g  3643  elimhyp  4543  elimhyp2v  4544  elimhyp3v  4545  elimhyp4v  4546  elpwi  4559  elsni  4596  elpri  4603  eltpi  4644  snssi  4741  prssi  4776  snelpwi  5408  prelpwi  5411  elxpi  5665  releldmb  5918  relelrnb  5919  elrnmpt2d  5938  eloni  6350  limuni2  6403  funeu  6540  fneu  6625  fvelima2  6913  fvelima  6926  fvelimad  6928  eloprabi  8038  fo2ndf  8093  orderseqlem  8130  tfrlem9  8349  oeeulem  8564  elqsi  8740  qsel  8771  ecopovsym  8794  elpmi  8820  elmapi  8823  pmsspw  8852  brdomi  8933  en0  8992  en0r  8994  en1  8998  mapdom1  9107  rexdif1en  9122  ominf  9201  unblem2  9230  unfilem1  9242  fodomfir  9265  fiin  9361  brwdomi  9509  canthwdom  9520  brwdom3i  9524  unxpwdom  9530  scott0  9837  acni  9994  djuinf  10138  pwdjudom  10164  fin1ai  10243  fin2i  10245  fin4i  10248  ssfin3ds  10280  fin23lem17  10288  fin23lem38  10299  fin23lem39  10300  isfin32i  10315  fin34  10340  isfin7-2  10346  fin1a2lem13  10362  fin12  10363  gchi  10575  wuntr  10656  wununi  10657  wunpw  10658  wunpr  10660  wun0  10669  tskpwss  10703  tskpw  10704  tsken  10705  grutr  10744  grupw  10746  grupr  10748  gruurn  10749  ingru  10766  indpi  10858  eliooord  13402  fzrev3i  13589  fzne1  13602  elfzole1  13666  elfzolt2  13667  bcp1nk  14323  rere  15139  nn0abscl  15329  climcl  15516  rlimcl  15520  rlimdm  15568  o1res  15577  rlimdmo1  15635  climcau  15688  caucvgb  15697  fprodcnv  16003  cshws0  17127  restsspw  17450  mreiincl  17614  catidex  17696  catcocl  17707  catass  17708  homa1  18060  homahom2  18061  odulat  18457  dlatjmdi  18548  psrel  18591  psref2  18592  pstr2  18593  reldir  18621  dirdm  18622  dirref  18623  dirtr  18624  dirge  18625  chnub  18644  mgmcl  18667  submgmss  18729  submgmcl  18731  submgmmgm  18732  submss  18833  subm0cl  18835  submcl  18836  submmnd  18837  efmndbasf  18899  subgsubm  19180  symgbasf1o  19405  symginv  19432  psgneu  19536  odmulg  19586  frgpnabl  19905  dprdgrp  20037  dprdf  20038  abvfge0  20850  abveq0  20854  abvmul  20857  abvtri  20858  orngsqr  20902  lbsss  21131  lbssp  21133  lbsind  21134  domnchr  21571  cssi  21723  linds1  21849  linds2  21850  lindsind  21856  opsrtoslem2  22096  opsrso  22098  mdetunilem9  22667  uniopn  22944  iunopn  22945  inopn  22946  fiinopn  22948  eltpsg  22990  basis1  22997  basis2  22998  eltg4i  23007  lmff  23348  t1sep2  23416  cmpfii  23456  ptfinfin  23566  kqhmph  23866  fbasne0  23877  0nelfb  23878  fbsspw  23879  fbasssin  23883  ufli  23961  uffixfr  23970  elfm  23994  fclsopni  24062  fclselbas  24063  ustssxp  24252  ustbasel  24254  ustincl  24255  ustdiag  24256  ustinvel  24257  ustexhalf  24258  ustfilxp  24260  ustbas2  24272  ustbas  24274  psmetf  24353  psmet0  24355  psmettri2  24356  metflem  24375  xmetf  24376  xmeteq0  24385  xmettri2  24387  tmsxms  24533  tmsms  24534  metustsym  24602  tngnrg  24721  cncff  24942  cncfi  24943  cfili  25317  iscmet3lem2  25341  mbfres  25693  mbfimaopnlem  25704  limcresi  25934  dvcnp2  25969  ulmcl  26431  ulmf  26432  ulmcau  26445  pserulm  26472  pserdvlem2  26478  sinq34lt0t  26561  logtayl  26712  dchrmhm  27292  lgsdir2lem2  27377  2sqlem9  27478  mulog2sum  27588  newbdayim  27983  eleei  29054  uhgrf  29219  ushgrf  29220  upgrf  29243  umgrf  29255  uspgrf  29311  usgrf  29312  usgrfs  29314  nbcplgr  29591  clwlkcompim  29936  tncp  30637  eulplig  30644  grpofo  30658  grpolidinv  30660  grpoass  30662  nvvop  30768  phpar  30983  pjch1  31829  nn0mnfxrd  32913  toslub  33111  tosglb  33113  suppgsumssiun  33212  exsslsb  33854  fldextsubrg  33906  fldextress  33908  zhmnrg  34222  issgon  34380  measfrge0  34460  measvnul  34463  measvun  34466  fzssfzo  34796  bnj916  35188  bnj983  35206  cplgredgex  35431  acycgrcycl  35457  mfsdisj  35860  mtyf2  35861  maxsta  35864  mvtinf  35865  r1peuqusdeg1  35953  hfun  36488  hfsn  36489  hfelhf  36491  hfuni  36494  hfpw  36495  fneuni  36667  elttcirr  36851  curryset  37391  mptsnunlem  37792  heibor1lem  38268  heiborlem1  38270  heiborlem3  38272  opidonOLD  38311  isexid2  38314  elrelsrelim  38902  presucmap  38954  eqvrelqsel  39159  eldisjsim1  39393  elpcliN  40477  lnrfg  43656  sdomne0  43949  sdomne0d  43950  pwinfi2  44098  frege55lem1c  44452  gneispacef  44671  gneispacef2  44672  gneispacern2  44675  gneispace0nelrn  44676  gneispaceel  44679  gneispacess  44681  mnuop123d  44798  trintALTVD  45415  trintALT  45416  eliuniin  45637  eliuniin2  45658  disjrnmpt2  45726  stoweidlem35  46569  saluncl  46851  saldifcl  46853  0sal  46854  sge0resplit  46940  omedm  47033  funressneu  47601  afvelrnb0  47718  afvelima  47721  rlimdmafv  47731  funressndmafv2rn  47777  rlimdmafv2  47812  elsetpreimafv  47951  oexpnegALTV  48259  gricbri  48498  grlimprop2  48568  grilcbri  48591  asslawass  48775  linindsi  49029  inisegn0a  49417  eloprab1st2nd  49449  uobrcl  49774  uobeq2  49982  isinito2  50080  basrestermcfolem  50152  discsnterm  50155  islmd  50246