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  elimhOLD  1075  elab3gf  3670  elimhyp  4528  elimhyp2v  4529  elimhyp3v  4530  elimhyp4v  4531  elpwi  4549  elsni  4576  elpri  4581  eltpi  4617  snssi  4733  prssi  4746  prelpwi  5330  elxpi  5570  releldmb  5809  relelrnb  5810  elrnmpt2d  5827  elpredim  6153  eloni  6194  limuni2  6245  funeu  6373  fneu  6454  fvelima  6724  fvelimad  6725  eloprabi  7753  fo2ndf  7809  tfrlem9  8013  oeeulem  8219  elqsi  8342  qsel  8368  ecopovsym  8391  elpmi  8417  elmapi  8420  pmsspw  8433  brdomi  8512  undom  8597  mapdom1  8674  ominf  8722  unblem2  8763  unfilem1  8774  fiin  8878  brwdomi  9024  canthwdom  9035  brwdom3i  9039  unxpwdom  9045  scott0  9307  acni  9463  djuinf  9606  pwdjudom  9630  fin1ai  9707  fin2i  9709  fin4i  9712  ssfin3ds  9744  fin23lem17  9752  fin23lem38  9763  fin23lem39  9764  isfin32i  9779  fin34  9804  isfin7-2  9810  fin1a2lem13  9826  fin12  9827  gchi  10038  wuntr  10119  wununi  10120  wunpw  10121  wunpr  10123  wun0  10132  tskpwss  10166  tskpw  10167  tsken  10168  grutr  10207  grupw  10209  grupr  10211  gruurn  10212  ingru  10229  indpi  10321  eliooord  12788  fzrev3i  12966  elfzole1  13038  elfzolt2  13039  bcp1nk  13669  rere  14473  nn0abscl  14664  climcl  14848  rlimcl  14852  rlimdm  14900  o1res  14909  rlimdmo1  14966  climcau  15019  caucvgb  15028  fprodcnv  15329  cshws0  16427  restsspw  16697  mreiincl  16859  catidex  16937  catcocl  16948  catass  16949  homa1  17289  homahom2  17290  odulat  17747  dlatjmdi  17799  psrel  17805  psref2  17806  pstr2  17807  reldir  17835  dirdm  17836  dirref  17837  dirtr  17838  dirge  17839  mgmcl  17847  submss  17966  subm0cl  17968  submcl  17969  submmnd  17970  efmndbasf  18032  subgsubm  18293  symgbasf1o  18495  symginv  18522  psgneu  18626  odmulg  18675  frgpnabl  18987  dprdgrp  19119  dprdf  19120  abvfge0  19585  abveq0  19589  abvmul  19592  abvtri  19593  lbsss  19841  lbssp  19843  lbsind  19844  opsrtoslem2  20257  opsrso  20259  domnchr  20671  cssi  20820  linds1  20946  linds2  20947  lindsind  20953  mdetunilem9  21221  uniopn  21497  iunopn  21498  inopn  21499  fiinopn  21501  eltpsg  21543  basis1  21550  basis2  21551  eltg4i  21560  lmff  21901  t1sep2  21969  cmpfii  22009  ptfinfin  22119  kqhmph  22419  fbasne0  22430  0nelfb  22431  fbsspw  22432  fbasssin  22436  ufli  22514  uffixfr  22523  elfm  22547  fclsopni  22615  fclselbas  22616  ustssxp  22805  ustbasel  22807  ustincl  22808  ustdiag  22809  ustinvel  22810  ustexhalf  22811  ustfilxp  22813  ustbas2  22826  ustbas  22828  psmetf  22908  psmet0  22910  psmettri2  22911  metflem  22930  xmetf  22931  xmeteq0  22940  xmettri2  22942  tmsxms  23088  tmsms  23089  metustsym  23157  tngnrg  23275  cncff  23493  cncfi  23494  cfili  23863  iscmet3lem2  23887  mbfres  24237  mbfimaopnlem  24248  limcresi  24475  dvcnp2  24509  ulmcl  24961  ulmf  24962  ulmcau  24975  pserulm  25002  pserdvlem2  25008  sinq34lt0t  25087  logtayl  25235  dchrmhm  25809  lgsdir2lem2  25894  2sqlem9  25995  mulog2sum  26105  eleei  26675  uhgrf  26839  ushgrf  26840  upgrf  26863  umgrf  26875  uspgrf  26931  usgrf  26932  usgrfs  26934  nbcplgr  27208  clwlkcompim  27553  tncp  28247  eulplig  28254  grpofo  28268  grpolidinv  28270  grpoass  28272  nvvop  28378  phpar  28593  pjch1  29439  fzne1  30503  toslub  30648  tosglb  30650  orngsqr  30870  fldextsubrg  31034  fldextress  31035  zhmnrg  31201  issgon  31375  measfrge0  31455  measvnul  31458  measvun  31461  fzssfzo  31802  bnj916  32198  bnj983  32216  cplgredgex  32360  acycgrcycl  32387  mfsdisj  32790  mtyf2  32791  maxsta  32794  mvtinf  32795  orderseqlem  33087  hfun  33632  hfsn  33633  hfelhf  33635  hfuni  33638  hfpw  33639  fneuni  33688  curryset  34250  mptsnunlem  34611  heibor1lem  35079  heiborlem1  35081  heiborlem3  35083  opidonOLD  35122  isexid2  35125  elrelsrelim  35720  eqvrelqsel  35843  elpcliN  37021  lnrfg  39709  pwinfi2  39911  frege55lem1c  40252  gneispacef  40475  gneispacef2  40476  gneispacern2  40479  gneispace0nelrn  40480  gneispaceel  40483  gneispacess  40485  mnuop123d  40588  trintALTVD  41204  trintALT  41205  eliuniin  41355  eliuniin2  41376  disjrnmpt2  41438  fvelima2  41521  stoweidlem35  42310  saluncl  42592  saldifcl  42594  0sal  42595  sge0resplit  42678  omedm  42771  funressneu  43272  afvelrnb0  43353  afvelima  43356  rlimdmafv  43366  funressndmafv2rn  43412  rlimdmafv2  43447  elsetpreimafv  43535  oexpnegALTV  43832  isisomgr  43979  submgmss  44049  submgmcl  44051  submgmmgm  44052  asslawass  44090  linindsi  44492