Theorem ibi 270

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		ibi.1	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	1, 2	mpbid 235	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ibir  271  elab3gf  3646  elab3g  3647  elimhyp  4558  elimhyp2v  4559  elimhyp3v  4560  elimhyp4v  4561  elpwi  4574  elsni  4611  elpri  4618  eltpi  4659  snssi  4756  prssi  4792  snelpwi  5430  prelpwi  5433  elxpi  5688  releldmb  5941  relelrnb  5942  elrnmpt2d  5961  eloni  6377  limuni2  6431  funeu  6568  fneu  6652  fvelima2  6940  fvelima  6953  fvelimad  6955  eloprabi  8069  fo2ndf  8125  orderseqlem  8162  tfrlem9  8381  oeeulem  8596  elqsi  8772  qsel  8803  ecopovsym  8826  elpmi  8852  elmapi  8855  pmsspw  8884  brdomi  8965  en0  9024  en0r  9026  en1  9030  mapdom1  9140  rexdif1en  9155  ominf  9234  unblem2  9263  unfilem1  9275  fodomfir  9297  fiin  9392  brwdomi  9540  canthwdom  9551  brwdom3i  9555  unxpwdom  9561  scott0b  9876  scott0OLD  9877  acni  10048  djuinf  10191  pwdjudom  10217  fin1ai  10295  fin2i  10297  fin4i  10300  ssfin3ds  10332  fin23lem17  10340  fin23lem38  10351  fin23lem39  10352  isfin32i  10367  fin34  10392  isfin7-2  10398  fin1a2lem13  10414  fin12  10415  gchi  10627  wuntr  10708  wununi  10709  wunpw  10710  wunpr  10712  wun0  10721  tskpwss  10755  tskpw  10756  tsken  10757  grutr  10796  grupw  10798  grupr  10800  gruurn  10801  ingru  10818  indpi  10910  eliooord  13450  fzrev3i  13638  fzne1  13651  elfzole1  13715  elfzolt2  13716  bcp1nk  14373  rere  15199  nn0abscl  15389  climcl  15576  rlimcl  15580  rlimdm  15628  o1res  15637  rlimdmo1  15695  climcau  15748  caucvgb  15757  fprodcnv  16063  cshws0  17186  restsspw  17509  mreiincl  17673  catidex  17755  catcocl  17766  catass  17767  homa1  18119  homahom2  18120  odulat  18516  dlatjmdi  18607  psrel  18650  psref2  18651  pstr2  18652  reldir  18680  dirdm  18681  dirref  18682  dirtr  18683  dirge  18684  chnub  18703  mgmcl  18726  submgmss  18792  submgmcl  18794  submgmmgm  18795  submss  18898  subm0cl  18900  submcl  18901  submmnd  18903  efmndbasf  18965  subgsubm  19246  symgbasf1o  19476  symginv  19503  psgneu  19607  odmulg  19657  frgpnabl  19976  dprdgrp  20108  dprdf  20109  abvfge0  20954  abveq0  20958  abvmul  20961  abvtri  20962  orngsqr  21006  lbsss  21235  lbssp  21237  lbsind  21238  domnchr  21719  cssi  21871  linds1  21997  linds2  21998  lindsind  22004  opsrtoslem2  22244  opsrso  22246  mdetunilem9  22814  uniopn  23091  iunopn  23092  inopn  23093  fiinopn  23095  eltpsg  23137  basis1  23144  basis2  23145  eltg4i  23154  lmff  23495  t1sep2  23563  cmpfii  23603  ptfinfin  23713  kqhmph  24013  fbasne0  24024  0nelfb  24025  fbsspw  24026  fbasssin  24030  ufli  24108  uffixfr  24117  elfm  24141  fclsopni  24209  fclselbas  24210  ustssxp  24399  ustbasel  24401  ustincl  24402  ustdiag  24403  ustinvel  24404  ustexhalf  24405  ustfilxp  24407  ustbas2  24419  ustbas  24421  psmetf  24500  psmet0  24502  psmettri2  24503  metflem  24522  xmetf  24523  xmeteq0  24532  xmettri2  24534  tmsxms  24680  tmsms  24681  metustsym  24749  tngnrg  24868  cncff  25089  cncfi  25090  cfili  25464  iscmet3lem2  25488  mbfres  25840  mbfimaopnlem  25851  limcresi  26081  dvcnp2  26116  ulmcl  26581  ulmf  26582  ulmcau  26595  pserulm  26622  pserdvlem2  26628  sinq34lt0t  26711  logtayl  26862  dchrmhm  27442  lgsdir2lem2  27527  2sqlem9  27628  mulog2sum  27738  newbdayim  28133  eleei  29284  uhgrf  29449  ushgrf  29450  upgrf  29473  umgrf  29485  uspgrf  29541  usgrf  29542  usgrfs  29544  nbcplgr  29821  clwlkcompim  30166  tncp  30867  eulplig  30874  grpofo  30888  grpolidinv  30890  grpoass  30892  nvvop  30998  phpar  31213  pjch1  32059  nn0mnfxrd  33133  toslub  33324  tosglb  33326  suppgsumssiun  33423  exsslsb  34018  fldextsubrg  34070  fldextress  34072  zhmnrg  34386  issgon  34544  measfrge0  34625  measvnul  34628  measvun  34631  fzssfzo  34961  bnj916  35353  bnj983  35371  elkarden  35592  cplgredgex  35634  acycgrcycl  35660  mfsdisj  36063  mtyf2  36064  maxsta  36067  mvtinf  36068  r1peuqusdeg1  36156  hfun  36691  hfsn  36692  hfelhf  36694  hfuni  36697  hfpw  36698  fneuni  36899  elttcirr  37083  curryset  37623  mptsnunlem  38025  heibor1lem  38501  heiborlem1  38503  heiborlem3  38505  opidonOLD  38544  isexid2  38547  elrelsrelim  39133  presucmap  39185  eqvrelqsel  39390  eldisjsim1  39624  elpcliN  40708  lnrfg  43887  sdomne0  44180  sdomne0d  44181  pwinfi2  44329  frege55lem1c  44683  gneispacef  44902  gneispacef2  44903  gneispacern2  44906  gneispace0nelrn  44907  gneispaceel  44910  gneispacess  44912  mnuop123d  45013  trintALTVD  45629  trintALT  45630  eliuniin  45858  eliuniin2  45879  disjrnmpt2  45947  stoweidlem35  46790  saluncl  47072  saldifcl  47074  0sal  47075  sge0resplit  47161  omedm  47254  funressneu  47825  afvelrnb0  47942  afvelima  47945  rlimdmafv  47955  funressndmafv2rn  48001  rlimdmafv2  48036  elsetpreimafv  48175  oexpnegALTV  48483  gricbri  48722  grlimprop2  48792  grilcbri  48815  asslawass  48999  linindsi  49268  inisegn0a  49655  eloprab1st2nd  49687  uobrcl  50012  uobeq2  50220  isinito2  50318  basrestermcfolem  50390  discsnterm  50393  islmd  50484