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  3643  elab3g  3644  elimhyp  4545  elimhyp2v  4546  elimhyp3v  4547  elimhyp4v  4548  elpwi  4561  elsni  4598  elpri  4605  eltpi  4646  snssi  4743  prssi  4778  snelpwi  5410  prelpwi  5413  elxpi  5667  releldmb  5920  relelrnb  5921  elrnmpt2d  5940  eloni  6352  limuni2  6405  funeu  6542  fneu  6627  fvelima2  6915  fvelima  6928  fvelimad  6930  eloprabi  8040  fo2ndf  8095  orderseqlem  8132  tfrlem9  8351  oeeulem  8566  elqsi  8742  qsel  8773  ecopovsym  8796  elpmi  8823  elmapi  8826  pmsspw  8855  brdomi  8936  en0  8995  en0r  8997  en1  9001  mapdom1  9110  rexdif1en  9125  ominf  9204  unblem2  9233  unfilem1  9245  fodomfir  9268  fiin  9365  brwdomi  9513  canthwdom  9524  brwdom3i  9528  unxpwdom  9534  scott0  9841  acni  9998  djuinf  10142  pwdjudom  10168  fin1ai  10247  fin2i  10249  fin4i  10252  ssfin3ds  10284  fin23lem17  10292  fin23lem38  10303  fin23lem39  10304  isfin32i  10319  fin34  10344  isfin7-2  10350  fin1a2lem13  10366  fin12  10367  gchi  10579  wuntr  10660  wununi  10661  wunpw  10662  wunpr  10664  wun0  10673  tskpwss  10707  tskpw  10708  tsken  10709  grutr  10748  grupw  10750  grupr  10752  gruurn  10753  ingru  10770  indpi  10862  eliooord  13406  fzrev3i  13593  fzne1  13606  elfzole1  13670  elfzolt2  13671  bcp1nk  14327  rere  15132  nn0abscl  15322  climcl  15509  rlimcl  15513  rlimdm  15561  o1res  15570  rlimdmo1  15628  climcau  15681  caucvgb  15690  fprodcnv  15996  cshws0  17120  restsspw  17443  mreiincl  17607  catidex  17689  catcocl  17700  catass  17701  homa1  18053  homahom2  18054  odulat  18450  dlatjmdi  18541  psrel  18584  psref2  18585  pstr2  18586  reldir  18614  dirdm  18615  dirref  18616  dirtr  18617  dirge  18618  chnub  18637  mgmcl  18660  submgmss  18722  submgmcl  18724  submgmmgm  18725  submss  18826  subm0cl  18828  submcl  18829  submmnd  18830  efmndbasf  18892  subgsubm  19173  symgbasf1o  19398  symginv  19425  psgneu  19529  odmulg  19579  frgpnabl  19898  dprdgrp  20030  dprdf  20031  abvfge0  20843  abveq0  20847  abvmul  20850  abvtri  20851  orngsqr  20895  lbsss  21124  lbssp  21126  lbsind  21127  domnchr  21564  cssi  21716  linds1  21842  linds2  21843  lindsind  21849  opsrtoslem2  22089  opsrso  22091  mdetunilem9  22660  uniopn  22937  iunopn  22938  inopn  22939  fiinopn  22941  eltpsg  22983  basis1  22990  basis2  22991  eltg4i  23000  lmff  23341  t1sep2  23409  cmpfii  23449  ptfinfin  23559  kqhmph  23859  fbasne0  23870  0nelfb  23871  fbsspw  23872  fbasssin  23876  ufli  23954  uffixfr  23963  elfm  23987  fclsopni  24055  fclselbas  24056  ustssxp  24245  ustbasel  24247  ustincl  24248  ustdiag  24249  ustinvel  24250  ustexhalf  24251  ustfilxp  24253  ustbas2  24265  ustbas  24267  psmetf  24346  psmet0  24348  psmettri2  24349  metflem  24368  xmetf  24369  xmeteq0  24378  xmettri2  24380  tmsxms  24526  tmsms  24527  metustsym  24595  tngnrg  24714  cncff  24935  cncfi  24936  cfili  25310  iscmet3lem2  25334  mbfres  25686  mbfimaopnlem  25697  limcresi  25927  dvcnp2  25962  ulmcl  26421  ulmf  26422  ulmcau  26435  pserulm  26462  pserdvlem2  26468  sinq34lt0t  26551  logtayl  26702  dchrmhm  27282  lgsdir2lem2  27367  2sqlem9  27468  mulog2sum  27578  newbdayim  27973  eleei  29044  uhgrf  29209  ushgrf  29210  upgrf  29233  umgrf  29245  uspgrf  29301  usgrf  29302  usgrfs  29304  nbcplgr  29581  clwlkcompim  29926  tncp  30627  eulplig  30634  grpofo  30648  grpolidinv  30650  grpoass  30652  nvvop  30758  phpar  30973  pjch1  31819  nn0mnfxrd  32903  toslub  33112  tosglb  33114  suppgsumssiun  33213  exsslsb  33855  fldextsubrg  33907  fldextress  33909  zhmnrg  34223  issgon  34381  measfrge0  34461  measvnul  34464  measvun  34467  fzssfzo  34797  bnj916  35192  bnj983  35210  cplgredgex  35435  acycgrcycl  35461  mfsdisj  35864  mtyf2  35865  maxsta  35868  mvtinf  35869  r1peuqusdeg1  35957  hfun  36492  hfsn  36493  hfelhf  36495  hfuni  36498  hfpw  36499  fneuni  36671  elttcirr  36855  curryset  37395  mptsnunlem  37796  heibor1lem  38272  heiborlem1  38274  heiborlem3  38276  opidonOLD  38315  isexid2  38318  elrelsrelim  38906  presucmap  38958  eqvrelqsel  39163  eldisjsim1  39397  elpcliN  40481  lnrfg  43660  sdomne0  43953  sdomne0d  43954  pwinfi2  44102  frege55lem1c  44456  gneispacef  44675  gneispacef2  44676  gneispacern2  44679  gneispace0nelrn  44680  gneispaceel  44683  gneispacess  44685  mnuop123d  44802  trintALTVD  45419  trintALT  45420  eliuniin  45641  eliuniin2  45662  disjrnmpt2  45730  stoweidlem35  46573  saluncl  46855  saldifcl  46857  0sal  46858  sge0resplit  46944  omedm  47037  funressneu  47605  afvelrnb0  47722  afvelima  47725  rlimdmafv  47735  funressndmafv2rn  47781  rlimdmafv2  47816  elsetpreimafv  47955  oexpnegALTV  48263  gricbri  48502  grlimprop2  48572  grilcbri  48595  asslawass  48779  linindsi  49033  inisegn0a  49421  eloprab1st2nd  49453  uobrcl  49778  uobeq2  49986  isinito2  50084  basrestermcfolem  50156  discsnterm  50159  islmd  50250