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  3620  elimhyp  4488  elimhyp2v  4489  elimhyp3v  4490  elimhyp4v  4491  elpwi  4506  elsni  4542  elpri  4547  eltpi  4585  snssi  4701  prssi  4714  prelpwi  5305  elxpi  5541  releldmb  5780  relelrnb  5781  elrnmpt2d  5799  elpredim  6128  eloni  6169  limuni2  6220  funeu  6349  fneu  6432  fvelima  6706  fvelimad  6707  eloprabi  7743  fo2ndf  7800  tfrlem9  8004  oeeulem  8210  elqsi  8333  qsel  8359  ecopovsym  8382  elpmi  8408  elmapi  8411  pmsspw  8424  brdomi  8503  undom  8588  mapdom1  8666  ominf  8714  unblem2  8755  unfilem1  8766  fiin  8870  brwdomi  9016  canthwdom  9027  brwdom3i  9031  unxpwdom  9037  scott0  9299  acni  9456  djuinf  9599  pwdjudom  9627  fin1ai  9704  fin2i  9706  fin4i  9709  ssfin3ds  9741  fin23lem17  9749  fin23lem38  9760  fin23lem39  9761  isfin32i  9776  fin34  9801  isfin7-2  9807  fin1a2lem13  9823  fin12  9824  gchi  10035  wuntr  10116  wununi  10117  wunpw  10118  wunpr  10120  wun0  10129  tskpwss  10163  tskpw  10164  tsken  10165  grutr  10204  grupw  10206  grupr  10208  gruurn  10209  ingru  10226  indpi  10318  eliooord  12784  fzrev3i  12969  elfzole1  13041  elfzolt2  13042  bcp1nk  13673  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  18988  dprdgrp  19120  dprdf  19121  abvfge0  19586  abveq0  19590  abvmul  19593  abvtri  19594  lbsss  19842  lbssp  19844  lbsind  19845  domnchr  20224  cssi  20373  linds1  20499  linds2  20500  lindsind  20506  opsrtoslem2  20724  opsrso  20726  mdetunilem9  21225  uniopn  21502  iunopn  21503  inopn  21504  fiinopn  21506  eltpsg  21548  basis1  21555  basis2  21556  eltg4i  21565  lmff  21906  t1sep2  21974  cmpfii  22014  ptfinfin  22124  kqhmph  22424  fbasne0  22435  0nelfb  22436  fbsspw  22437  fbasssin  22441  ufli  22519  uffixfr  22528  elfm  22552  fclsopni  22620  fclselbas  22621  ustssxp  22810  ustbasel  22812  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  ustfilxp  22818  ustbas2  22831  ustbas  22833  psmetf  22913  psmet0  22915  psmettri2  22916  metflem  22935  xmetf  22936  xmeteq0  22945  xmettri2  22947  tmsxms  23093  tmsms  23094  metustsym  23162  tngnrg  23280  cncff  23498  cncfi  23499  cfili  23872  iscmet3lem2  23896  mbfres  24248  mbfimaopnlem  24259  limcresi  24488  dvcnp2  24523  ulmcl  24976  ulmf  24977  ulmcau  24990  pserulm  25017  pserdvlem2  25023  sinq34lt0t  25102  logtayl  25251  dchrmhm  25825  lgsdir2lem2  25910  2sqlem9  26011  mulog2sum  26121  eleei  26691  uhgrf  26855  ushgrf  26856  upgrf  26879  umgrf  26891  uspgrf  26947  usgrf  26948  usgrfs  26950  nbcplgr  27224  clwlkcompim  27569  tncp  28261  eulplig  28268  grpofo  28282  grpolidinv  28284  grpoass  28286  nvvop  28392  phpar  28607  pjch1  29453  fzne1  30537  toslub  30681  tosglb  30683  orngsqr  30928  fldextsubrg  31129  fldextress  31130  zhmnrg  31318  issgon  31492  measfrge0  31572  measvnul  31575  measvun  31578  fzssfzo  31919  bnj916  32315  bnj983  32333  cplgredgex  32480  acycgrcycl  32507  mfsdisj  32910  mtyf2  32911  maxsta  32914  mvtinf  32915  orderseqlem  33207  hfun  33752  hfsn  33753  hfelhf  33755  hfuni  33758  hfpw  33759  fneuni  33808  curryset  34381  mptsnunlem  34755  heibor1lem  35247  heiborlem1  35249  heiborlem3  35251  opidonOLD  35290  isexid2  35293  elrelsrelim  35888  eqvrelqsel  36011  elpcliN  37189  lnrfg  40063  pwinfi2  40261  frege55lem1c  40617  gneispacef  40838  gneispacef2  40839  gneispacern2  40842  gneispace0nelrn  40843  gneispaceel  40846  gneispacess  40848  mnuop123d  40970  trintALTVD  41586  trintALT  41587  eliuniin  41735  eliuniin2  41755  disjrnmpt2  41815  fvelima2  41898  stoweidlem35  42677  saluncl  42959  saldifcl  42961  0sal  42962  sge0resplit  43045  omedm  43138  funressneu  43639  afvelrnb0  43720  afvelima  43723  rlimdmafv  43733  funressndmafv2rn  43779  rlimdmafv2  43814  elsetpreimafv  43902  oexpnegALTV  44195  isisomgr  44342  submgmss  44412  submgmcl  44414  submgmmgm  44415  asslawass  44453  linindsi  44856