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  3638  elab3g  3639  elimhyp  4548  elimhyp2v  4549  elimhyp3v  4550  elimhyp4v  4551  elpwi  4564  elsni  4601  elpri  4608  eltpi  4649  snssi  4746  prssi  4782  snelpwi  5412  prelpwi  5415  elxpi  5673  releldmb  5928  relelrnb  5929  elrnmpt2d  5948  eloni  6365  limuni2  6419  funeu  6557  fneu  6641  fvelima2  6929  fvelima  6942  fvelimad  6944  eloprabi  8063  fo2ndf  8121  orderseqlem  8158  tfrlem9  8377  oeeulem  8594  elqsi  8770  qsel  8801  ecopovsym  8824  elpmi  8850  elmapi  8853  pmsspw  8889  brdomi  8970  en0  9029  en0r  9031  en1  9035  mapdom1  9145  rexdif1en  9160  ominf  9239  unblem2  9269  unfilem1  9281  fodomfir  9303  fiin  9398  brwdomi  9546  canthwdom  9557  brwdom3i  9561  unxpwdom  9567  hfelhfOLD  9897  hfunOLD  9900  hfsnOLD  9902  hfuniOLD  9906  hfpwOLD  9908  scott0b  9918  scott0OLD  9919  acni  10105  djuinf  10248  pwdjudom  10274  fin1ai  10352  fin2i  10354  fin4i  10357  ssfin3ds  10389  fin23lem17  10397  fin23lem38  10408  fin23lem39  10409  isfin32i  10424  fin34  10449  isfin7-2  10455  fin1a2lem13  10471  fin12  10472  gchi  10690  wuntr  10771  wununi  10772  wunpw  10773  wunpr  10775  wun0  10784  tskpwss  10818  tskpw  10819  tsken  10820  grutr  10859  grupw  10861  grupr  10863  gruurn  10864  ingru  10881  indpi  10973  eliooord  13517  fzrev3i  13705  fzne1  13718  elfzole1  13782  elfzolt2  13783  bcp1nk  14441  rere  15269  nn0abscl  15459  climcl  15646  rlimcl  15650  rlimdm  15698  o1res  15707  rlimdmo1  15765  climcau  15818  caucvgb  15827  fprodcnv  16130  cshws0  17259  restsspw  17582  mreiincl  17746  catidex  17828  catcocl  17839  catass  17840  homa1  18192  homahom2  18193  odulat  18589  dlatjmdi  18680  psrel  18723  psref2  18724  pstr2  18725  reldir  18753  dirdm  18754  dirref  18755  dirtr  18756  dirge  18757  chnub  18776  mgmcl  18799  submgmss  18874  submgmcl  18876  submgmmgm  18877  submss  18984  subm0cl  18986  submcl  18987  submmnd  18989  efmndbasf  19051  subgsubm  19339  symgbasf1o  19569  symginv  19596  psgneu  19700  odmulg  19750  frgpnabl  20069  dprdgrp  20201  dprdf  20202  abvfge0  21051  abveq0  21055  abvmul  21058  abvtri  21059  orngsqr  21103  lbsss  21332  lbssp  21334  lbsind  21335  domnchr  21818  cssi  21970  linds1  22096  linds2  22097  lindsind  22103  opsrtoslem2  22345  opsrso  22347  mdetunilem9  22915  uniopn  23195  iunopn  23196  inopn  23197  fiinopn  23199  eltpsg  23241  basis1  23248  basis2  23249  eltg4i  23258  lmff  23599  t1sep2  23667  cmpfii  23707  ptfinfin  23818  kqhmph  24118  fbasne0  24129  0nelfb  24130  fbsspw  24131  fbasssin  24135  ufli  24213  uffixfr  24222  elfm  24246  fclsopni  24314  fclselbas  24315  ustssxp  24504  ustbasel  24506  ustincl  24507  ustdiag  24508  ustinvel  24509  ustexhalf  24510  ustfilxp  24512  ustbas2  24524  ustbas  24526  psmetf  24605  psmet0  24607  psmettri2  24608  metflem  24627  xmetf  24628  xmeteq0  24637  xmettri2  24639  tmsxms  24785  tmsms  24786  metustsym  24854  tngnrg  24973  cncff  25194  cncfi  25195  cfili  25569  iscmet3lem2  25593  mbfres  25945  mbfimaopnlem  25956  limcresi  26185  dvcnp2  26220  ulmcl  26690  ulmf  26691  ulmcau  26704  pserulm  26731  pserdvlem2  26737  sinq34lt0t  26820  logtayl  26970  dchrmhm  27550  lgsdir2lem2  27635  2sqlem9  27736  mulog2sum  27846  newbdayim  28271  eleei  29457  uhgrf  29622  ushgrf  29623  upgrf  29646  umgrf  29658  uspgrf  29717  usgrf  29718  usgrfs  29720  nbcplgr  29997  clwlkcompim  30349  acycgrcycl  30735  tncp  31062  eulplig  31069  grpofo  31083  grpolidinv  31085  grpoass  31087  nvvop  31193  phpar  31408  pjch1  32254  nn0mnfxrd  33325  toslub  33516  tosglb  33518  suppgsumssiun  33615  exsslsb  34211  fldextsubrg  34263  fldextress  34265  zhmnrg  34579  issgon  34737  measfrge0  34818  measvnul  34821  measvun  34824  fzssfzo  35154  bnj916  35546  bnj983  35564  elkarden  35796  cplgredgex  35874  mfsdisj  36284  mtyf2  36285  maxsta  36288  mvtinf  36289  r1peuqusdeg1  36377  fneuni  37105  elttcirr  37289  curryset  37829  mptsnunlem  38229  heibor1lem  38711  heiborlem1  38713  heiborlem3  38715  opidonOLD  38754  isexid2  38757  elrelsrelim  39343  presucmap  39395  eqvrelqsel  39600  eldisjsim1  39834  elpcliN  40918  lnrfg  44079  sdomne0  44372  sdomne0d  44373  pwinfi2  44521  frege55lem1c  44875  gneispacef  45094  gneispacef2  45095  gneispacern2  45098  gneispace0nelrn  45099  gneispaceel  45102  gneispacess  45104  mnuop123d  45205  trintALTVD  45821  trintALT  45822  eliuniin  46057  eliuniin2  46078  disjrnmpt2  46146  stoweidlem35  46989  saluncl  47271  saldifcl  47273  0sal  47274  sge0resplit  47360  omedm  47453  funressneu  48061  afvelrnb0  48178  afvelima  48181  rlimdmafv  48191  funressndmafv2rn  48237  rlimdmafv2  48272  elsetpreimafv  48411  oexpnegALTV  48719  gricbri  48958  grlimprop2  49028  grilcbri  49051  asslawass  49234  linindsi  49503  inisegn0a  49890  eloprab1st2nd  49922  uobrcl  50245  uobeq2  50453  isinito2  50551  basrestermcfolem  50623  discsnterm  50626  islmd  50717