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 22	. 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  3594  elimhyp  4483  elimhyp2v  4484  elimhyp3v  4485  elimhyp4v  4486  elpwi  4501  elsni  4537  elpri  4542  eltpi  4580  snssi  4696  prssi  4709  prelpwi  5306  elxpi  5544  releldmb  5785  relelrnb  5786  elrnmpt2d  5802  elpredim  6136  eloni  6177  limuni2  6228  funeu  6358  fneu  6441  fvelima  6717  fvelimad  6718  eloprabi  7763  fo2ndf  7820  tfrlem9  8029  oeeulem  8235  elqsi  8358  qsel  8384  ecopovsym  8407  elpmi  8433  elmapi  8436  pmsspw  8457  brdomi  8536  undom  8623  mapdom1  8701  ominf  8749  unblem2  8794  unfilem1  8805  fiin  8909  brwdomi  9055  canthwdom  9066  brwdom3i  9070  unxpwdom  9076  scott0  9338  acni  9495  djuinf  9638  pwdjudom  9666  fin1ai  9743  fin2i  9745  fin4i  9748  ssfin3ds  9780  fin23lem17  9788  fin23lem38  9799  fin23lem39  9800  isfin32i  9815  fin34  9840  isfin7-2  9846  fin1a2lem13  9862  fin12  9863  gchi  10074  wuntr  10155  wununi  10156  wunpw  10157  wunpr  10159  wun0  10168  tskpwss  10202  tskpw  10203  tsken  10204  grutr  10243  grupw  10245  grupr  10247  gruurn  10248  ingru  10265  indpi  10357  eliooord  12828  fzrev3i  13013  elfzole1  13085  elfzolt2  13086  bcp1nk  13717  rere  14519  nn0abscl  14710  climcl  14894  rlimcl  14898  rlimdm  14946  o1res  14955  rlimdmo1  15012  climcau  15065  caucvgb  15074  fprodcnv  15375  cshws0  16483  restsspw  16753  mreiincl  16915  catidex  16993  catcocl  17004  catass  17005  homa1  17353  homahom2  17354  odulat  17811  dlatjmdi  17863  psrel  17869  psref2  17870  pstr2  17871  reldir  17899  dirdm  17900  dirref  17901  dirtr  17902  dirge  17903  mgmcl  17911  submss  18030  subm0cl  18032  submcl  18033  submmnd  18034  efmndbasf  18096  subgsubm  18358  symgbasf1o  18560  symginv  18587  psgneu  18691  odmulg  18740  frgpnabl  19053  dprdgrp  19185  dprdf  19186  abvfge0  19651  abveq0  19655  abvmul  19658  abvtri  19659  lbsss  19907  lbssp  19909  lbsind  19910  domnchr  20290  cssi  20439  linds1  20565  linds2  20566  lindsind  20572  opsrtoslem2  20806  opsrso  20808  mdetunilem9  21310  uniopn  21587  iunopn  21588  inopn  21589  fiinopn  21591  eltpsg  21633  basis1  21640  basis2  21641  eltg4i  21650  lmff  21991  t1sep2  22059  cmpfii  22099  ptfinfin  22209  kqhmph  22509  fbasne0  22520  0nelfb  22521  fbsspw  22522  fbasssin  22526  ufli  22604  uffixfr  22613  elfm  22637  fclsopni  22705  fclselbas  22706  ustssxp  22895  ustbasel  22897  ustincl  22898  ustdiag  22899  ustinvel  22900  ustexhalf  22901  ustfilxp  22903  ustbas2  22916  ustbas  22918  psmetf  22998  psmet0  23000  psmettri2  23001  metflem  23020  xmetf  23021  xmeteq0  23030  xmettri2  23032  tmsxms  23178  tmsms  23179  metustsym  23247  tngnrg  23366  cncff  23584  cncfi  23585  cfili  23958  iscmet3lem2  23982  mbfres  24334  mbfimaopnlem  24345  limcresi  24574  dvcnp2  24609  ulmcl  25065  ulmf  25066  ulmcau  25079  pserulm  25106  pserdvlem2  25112  sinq34lt0t  25191  logtayl  25340  dchrmhm  25914  lgsdir2lem2  25999  2sqlem9  26100  mulog2sum  26210  eleei  26780  uhgrf  26944  ushgrf  26945  upgrf  26968  umgrf  26980  uspgrf  27036  usgrf  27037  usgrfs  27039  nbcplgr  27313  clwlkcompim  27658  tncp  28350  eulplig  28357  grpofo  28371  grpolidinv  28373  grpoass  28375  nvvop  28481  phpar  28696  pjch1  29542  fzne1  30623  toslub  30767  tosglb  30769  orngsqr  31019  fldextsubrg  31237  fldextress  31238  zhmnrg  31426  issgon  31600  measfrge0  31680  measvnul  31683  measvun  31686  fzssfzo  32027  bnj916  32423  bnj983  32441  cplgredgex  32588  acycgrcycl  32615  mfsdisj  33018  mtyf2  33019  maxsta  33022  mvtinf  33023  orderseqlem  33345  hfun  34019  hfsn  34020  hfelhf  34022  hfuni  34025  hfpw  34026  fneuni  34075  curryset  34652  mptsnunlem  35025  heibor1lem  35517  heiborlem1  35519  heiborlem3  35521  opidonOLD  35560  isexid2  35563  elrelsrelim  36158  eqvrelqsel  36281  elpcliN  37459  lnrfg  40426  pwinfi2  40624  frege55lem1c  40980  gneispacef  41201  gneispacef2  41202  gneispacern2  41205  gneispace0nelrn  41206  gneispaceel  41209  gneispacess  41211  mnuop123d  41333  trintALTVD  41949  trintALT  41950  eliuniin  42098  eliuniin2  42118  disjrnmpt2  42175  fvelima2  42256  stoweidlem35  43033  saluncl  43315  saldifcl  43317  0sal  43318  sge0resplit  43401  omedm  43494  funressneu  43995  afvelrnb0  44078  afvelima  44081  rlimdmafv  44091  funressndmafv2rn  44137  rlimdmafv2  44172  elsetpreimafv  44260  oexpnegALTV  44552  isisomgr  44699  submgmss  44769  submgmcl  44771  submgmmgm  44772  asslawass  44810  linindsi  45211