Theorem ibi 267

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ibir  268  elab3gf  3642  elab3g  3643  elimhyp  4544  elimhyp2v  4545  elimhyp3v  4546  elimhyp4v  4547  elpwi  4560  elsni  4596  elpri  4603  eltpi  4642  snssi  4762  prssi  4775  snelpwi  5390  prelpwi  5394  elxpi  5645  releldmb  5892  relelrnb  5893  elrnmpt2d  5912  eloni  6321  limuni2  6374  funeu  6511  fneu  6596  fvelima2  6879  fvelima  6892  fvelimad  6894  eloprabi  8005  fo2ndf  8061  orderseqlem  8097  tfrlem9  8314  oeeulem  8526  elqsi  8700  qsel  8730  ecopovsym  8753  elpmi  8780  elmapi  8783  pmsspw  8811  brdomi  8892  en0  8950  en0r  8952  en1  8956  mapdom1  9066  rexdif1en  9082  ominf  9163  ominfOLD  9164  unblem2  9198  unfilem1  9212  fodomfir  9237  fiin  9331  brwdomi  9479  canthwdom  9490  brwdom3i  9494  unxpwdom  9500  scott0  9801  acni  9958  djuinf  10102  pwdjudom  10128  fin1ai  10206  fin2i  10208  fin4i  10211  ssfin3ds  10243  fin23lem17  10251  fin23lem38  10262  fin23lem39  10263  isfin32i  10278  fin34  10303  isfin7-2  10309  fin1a2lem13  10325  fin12  10326  gchi  10537  wuntr  10618  wununi  10619  wunpw  10620  wunpr  10622  wun0  10631  tskpwss  10665  tskpw  10666  tsken  10667  grutr  10706  grupw  10708  grupr  10710  gruurn  10711  ingru  10728  indpi  10820  eliooord  13326  fzrev3i  13512  fzne1  13525  elfzole1  13588  elfzolt2  13589  bcp1nk  14242  rere  15047  nn0abscl  15237  climcl  15424  rlimcl  15428  rlimdm  15476  o1res  15485  rlimdmo1  15543  climcau  15596  caucvgb  15605  fprodcnv  15908  cshws0  17031  restsspw  17353  mreiincl  17516  catidex  17598  catcocl  17609  catass  17610  homa1  17962  homahom2  17963  odulat  18359  dlatjmdi  18450  psrel  18493  psref2  18494  pstr2  18495  reldir  18523  dirdm  18524  dirref  18525  dirtr  18526  dirge  18527  mgmcl  18535  submgmss  18597  submgmcl  18599  submgmmgm  18600  submss  18701  subm0cl  18703  submcl  18704  submmnd  18705  efmndbasf  18767  subgsubm  19045  symgbasf1o  19272  symginv  19299  psgneu  19403  odmulg  19453  frgpnabl  19772  dprdgrp  19904  dprdf  19905  abvfge0  20717  abveq0  20721  abvmul  20724  abvtri  20725  orngsqr  20769  lbsss  20999  lbssp  21001  lbsind  21002  domnchr  21457  cssi  21609  linds1  21735  linds2  21736  lindsind  21742  opsrtoslem2  21979  opsrso  21981  mdetunilem9  22523  uniopn  22800  iunopn  22801  inopn  22802  fiinopn  22804  eltpsg  22846  basis1  22853  basis2  22854  eltg4i  22863  lmff  23204  t1sep2  23272  cmpfii  23312  ptfinfin  23422  kqhmph  23722  fbasne0  23733  0nelfb  23734  fbsspw  23735  fbasssin  23739  ufli  23817  uffixfr  23826  elfm  23850  fclsopni  23918  fclselbas  23919  ustssxp  24108  ustbasel  24110  ustincl  24111  ustdiag  24112  ustinvel  24113  ustexhalf  24114  ustfilxp  24116  ustbas2  24129  ustbas  24131  psmetf  24210  psmet0  24212  psmettri2  24213  metflem  24232  xmetf  24233  xmeteq0  24242  xmettri2  24244  tmsxms  24390  tmsms  24391  metustsym  24459  tngnrg  24578  cncff  24802  cncfi  24803  cfili  25184  iscmet3lem2  25208  mbfres  25561  mbfimaopnlem  25572  limcresi  25802  dvcnp2  25837  dvcnp2OLD  25838  ulmcl  26306  ulmf  26307  ulmcau  26320  pserulm  26347  pserdvlem2  26354  sinq34lt0t  26434  logtayl  26585  dchrmhm  27168  lgsdir2lem2  27253  2sqlem9  27354  mulog2sum  27464  newbdayim  27835  eleei  28860  uhgrf  29025  ushgrf  29026  upgrf  29049  umgrf  29061  uspgrf  29117  usgrf  29118  usgrfs  29120  nbcplgr  29397  clwlkcompim  29743  tncp  30440  eulplig  30447  grpofo  30461  grpolidinv  30463  grpoass  30465  nvvop  30571  phpar  30786  pjch1  31632  toslub  32928  tosglb  32930  chnub  32967  exsslsb  33571  fldextsubrg  33624  fldextress  33626  zhmnrg  33934  issgon  34092  measfrge0  34172  measvnul  34175  measvun  34178  fzssfzo  34509  bnj916  34902  bnj983  34920  cplgredgex  35096  acycgrcycl  35122  mfsdisj  35525  mtyf2  35526  maxsta  35529  mvtinf  35530  r1peuqusdeg1  35618  hfun  36154  hfsn  36155  hfelhf  36157  hfuni  36160  hfpw  36161  fneuni  36323  curryset  36922  mptsnunlem  37314  heibor1lem  37791  heiborlem1  37793  heiborlem3  37795  opidonOLD  37834  isexid2  37837  elrelsrelim  38467  eqvrelqsel  38595  elpcliN  39875  lnrfg  43095  sdomne0  43389  sdomne0d  43390  pwinfi2  43538  frege55lem1c  43892  gneispacef  44111  gneispacef2  44112  gneispacern2  44115  gneispace0nelrn  44116  gneispaceel  44119  gneispacess  44121  mnuop123d  44238  trintALTVD  44856  trintALT  44857  eliuniin  45080  eliuniin2  45101  disjrnmpt2  45169  stoweidlem35  46020  saluncl  46302  saldifcl  46304  0sal  46305  sge0resplit  46391  omedm  46484  funressneu  47035  afvelrnb0  47152  afvelima  47155  rlimdmafv  47165  funressndmafv2rn  47211  rlimdmafv2  47246  elsetpreimafv  47373  oexpnegALTV  47665  gricbri  47904  grlimprop2  47974  grilcbri  47997  asslawass  48181  linindsi  48436  inisegn0a  48824  eloprab1st2nd  48856  uobrcl  49182  uobeq2  49390  isinito2  49488  basrestermcfolem  49560  discsnterm  49563  islmd  49654