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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ibir  271  elab3gf  3644  elab3g  3645  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elpwi  4570  elsni  4607  elpri  4614  eltpi  4655  snssi  4752  prssi  4788  snelpwi  5427  prelpwi  5430  elxpi  5685  releldmb  5938  relelrnb  5939  elrnmpt2d  5958  eloni  6372  limuni2  6426  funeu  6563  fneu  6647  fvelima2  6935  fvelima  6948  fvelimad  6950  eloprabi  8061  fo2ndf  8117  orderseqlem  8154  tfrlem9  8373  oeeulem  8588  elqsi  8764  qsel  8795  ecopovsym  8818  elpmi  8844  elmapi  8847  pmsspw  8876  brdomi  8957  en0  9016  en0r  9018  en1  9022  mapdom1  9131  rexdif1en  9146  ominf  9225  unblem2  9254  unfilem1  9266  fodomfir  9288  fiin  9383  brwdomi  9531  canthwdom  9542  brwdom3i  9546  unxpwdom  9552  scott0  9861  acni  10030  djuinf  10173  pwdjudom  10199  fin1ai  10278  fin2i  10280  fin4i  10283  ssfin3ds  10315  fin23lem17  10323  fin23lem38  10334  fin23lem39  10335  isfin32i  10350  fin34  10375  isfin7-2  10381  fin1a2lem13  10397  fin12  10398  gchi  10610  wuntr  10691  wununi  10692  wunpw  10693  wunpr  10695  wun0  10704  tskpwss  10738  tskpw  10739  tsken  10740  grutr  10779  grupw  10781  grupr  10783  gruurn  10784  ingru  10801  indpi  10893  eliooord  13433  fzrev3i  13621  fzne1  13634  elfzole1  13698  elfzolt2  13699  bcp1nk  14355  rere  15175  nn0abscl  15365  climcl  15552  rlimcl  15556  rlimdm  15604  o1res  15613  rlimdmo1  15671  climcau  15724  caucvgb  15733  fprodcnv  16039  cshws0  17162  restsspw  17485  mreiincl  17649  catidex  17731  catcocl  17742  catass  17743  homa1  18095  homahom2  18096  odulat  18492  dlatjmdi  18583  psrel  18626  psref2  18627  pstr2  18628  reldir  18656  dirdm  18657  dirref  18658  dirtr  18659  dirge  18660  chnub  18679  mgmcl  18702  submgmss  18764  submgmcl  18766  submgmmgm  18767  submss  18868  subm0cl  18870  submcl  18871  submmnd  18873  efmndbasf  18935  subgsubm  19216  symgbasf1o  19446  symginv  19473  psgneu  19577  odmulg  19627  frgpnabl  19946  dprdgrp  20078  dprdf  20079  abvfge0  20898  abveq0  20902  abvmul  20905  abvtri  20906  orngsqr  20950  lbsss  21179  lbssp  21181  lbsind  21182  domnchr  21663  cssi  21815  linds1  21941  linds2  21942  lindsind  21948  opsrtoslem2  22188  opsrso  22190  mdetunilem9  22758  uniopn  23035  iunopn  23036  inopn  23037  fiinopn  23039  eltpsg  23081  basis1  23088  basis2  23089  eltg4i  23098  lmff  23439  t1sep2  23507  cmpfii  23547  ptfinfin  23657  kqhmph  23957  fbasne0  23968  0nelfb  23969  fbsspw  23970  fbasssin  23974  ufli  24052  uffixfr  24061  elfm  24085  fclsopni  24153  fclselbas  24154  ustssxp  24343  ustbasel  24345  ustincl  24346  ustdiag  24347  ustinvel  24348  ustexhalf  24349  ustfilxp  24351  ustbas2  24363  ustbas  24365  psmetf  24444  psmet0  24446  psmettri2  24447  metflem  24466  xmetf  24467  xmeteq0  24476  xmettri2  24478  tmsxms  24624  tmsms  24625  metustsym  24693  tngnrg  24812  cncff  25033  cncfi  25034  cfili  25408  iscmet3lem2  25432  mbfres  25784  mbfimaopnlem  25795  limcresi  26025  dvcnp2  26060  ulmcl  26525  ulmf  26526  ulmcau  26539  pserulm  26566  pserdvlem2  26572  sinq34lt0t  26655  logtayl  26806  dchrmhm  27386  lgsdir2lem2  27471  2sqlem9  27572  mulog2sum  27682  newbdayim  28077  eleei  29228  uhgrf  29393  ushgrf  29394  upgrf  29417  umgrf  29429  uspgrf  29485  usgrf  29486  usgrfs  29488  nbcplgr  29765  clwlkcompim  30110  tncp  30811  eulplig  30818  grpofo  30832  grpolidinv  30834  grpoass  30836  nvvop  30942  phpar  31157  pjch1  32003  nn0mnfxrd  33077  toslub  33274  tosglb  33276  suppgsumssiun  33373  exsslsb  33968  fldextsubrg  34020  fldextress  34022  zhmnrg  34336  issgon  34494  measfrge0  34574  measvnul  34577  measvun  34580  fzssfzo  34910  bnj916  35302  bnj983  35320  elkarden  35549  cplgredgex  35594  acycgrcycl  35620  mfsdisj  36023  mtyf2  36024  maxsta  36027  mvtinf  36028  r1peuqusdeg1  36116  hfun  36651  hfsn  36652  hfelhf  36654  hfuni  36657  hfpw  36658  fneuni  36839  elttcirr  37023  curryset  37563  mptsnunlem  37965  heibor1lem  38441  heiborlem1  38443  heiborlem3  38445  opidonOLD  38484  isexid2  38487  elrelsrelim  39073  presucmap  39125  eqvrelqsel  39330  eldisjsim1  39564  elpcliN  40648  lnrfg  43829  sdomne0  44122  sdomne0d  44123  pwinfi2  44271  frege55lem1c  44625  gneispacef  44844  gneispacef2  44845  gneispacern2  44848  gneispace0nelrn  44849  gneispaceel  44852  gneispacess  44854  mnuop123d  44955  trintALTVD  45571  trintALT  45572  eliuniin  45800  eliuniin2  45821  disjrnmpt2  45889  stoweidlem35  46732  saluncl  47014  saldifcl  47016  0sal  47017  sge0resplit  47103  omedm  47196  funressneu  47767  afvelrnb0  47884  afvelima  47887  rlimdmafv  47897  funressndmafv2rn  47943  rlimdmafv2  47978  elsetpreimafv  48117  oexpnegALTV  48425  gricbri  48664  grlimprop2  48734  grilcbri  48757  asslawass  48941  linindsi  49210  inisegn0a  49597  eloprab1st2nd  49629  uobrcl  49954  uobeq2  50162  isinito2  50260  basrestermcfolem  50332  discsnterm  50335  islmd  50426