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  3653  elab3g  3654  elimhyp  4556  elimhyp2v  4557  elimhyp3v  4558  elimhyp4v  4559  elpwi  4572  elsni  4608  elpri  4615  eltpi  4654  snssi  4774  prssi  4787  snelpwi  5405  prelpwi  5409  elxpi  5662  releldmb  5912  relelrnb  5913  elrnmpt2d  5932  eloni  6344  limuni2  6397  funeu  6543  fneu  6630  fvelima2  6915  fvelima  6928  fvelimad  6930  eloprabi  8044  fo2ndf  8102  orderseqlem  8138  tfrlem9  8355  oeeulem  8567  elqsi  8741  qsel  8771  ecopovsym  8794  elpmi  8821  elmapi  8824  pmsspw  8852  brdomi  8933  en0  8991  en0r  8993  en1  8997  undomOLD  9033  mapdom1  9111  rexdif1en  9127  ominf  9211  ominfOLD  9212  unblem2  9246  unfilem1  9260  fodomfir  9285  fiin  9379  brwdomi  9527  canthwdom  9538  brwdom3i  9542  unxpwdom  9548  scott0  9845  acni  10004  djuinf  10148  pwdjudom  10174  fin1ai  10252  fin2i  10254  fin4i  10257  ssfin3ds  10289  fin23lem17  10297  fin23lem38  10308  fin23lem39  10309  isfin32i  10324  fin34  10349  isfin7-2  10355  fin1a2lem13  10371  fin12  10372  gchi  10583  wuntr  10664  wununi  10665  wunpw  10666  wunpr  10668  wun0  10677  tskpwss  10711  tskpw  10712  tsken  10713  grutr  10752  grupw  10754  grupr  10756  gruurn  10757  ingru  10774  indpi  10866  eliooord  13372  fzrev3i  13558  fzne1  13571  elfzole1  13634  elfzolt2  13635  bcp1nk  14288  rere  15094  nn0abscl  15284  climcl  15471  rlimcl  15475  rlimdm  15523  o1res  15532  rlimdmo1  15590  climcau  15643  caucvgb  15652  fprodcnv  15955  cshws0  17078  restsspw  17400  mreiincl  17563  catidex  17641  catcocl  17652  catass  17653  homa1  18005  homahom2  18006  odulat  18400  dlatjmdi  18491  psrel  18534  psref2  18535  pstr2  18536  reldir  18564  dirdm  18565  dirref  18566  dirtr  18567  dirge  18568  mgmcl  18576  submgmss  18638  submgmcl  18640  submgmmgm  18641  submss  18742  subm0cl  18744  submcl  18745  submmnd  18746  efmndbasf  18808  subgsubm  19086  symgbasf1o  19311  symginv  19338  psgneu  19442  odmulg  19492  frgpnabl  19811  dprdgrp  19943  dprdf  19944  abvfge0  20729  abveq0  20733  abvmul  20736  abvtri  20737  lbsss  20990  lbssp  20992  lbsind  20993  domnchr  21448  cssi  21599  linds1  21725  linds2  21726  lindsind  21732  opsrtoslem2  21969  opsrso  21971  mdetunilem9  22513  uniopn  22790  iunopn  22791  inopn  22792  fiinopn  22794  eltpsg  22836  basis1  22843  basis2  22844  eltg4i  22853  lmff  23194  t1sep2  23262  cmpfii  23302  ptfinfin  23412  kqhmph  23712  fbasne0  23723  0nelfb  23724  fbsspw  23725  fbasssin  23729  ufli  23807  uffixfr  23816  elfm  23840  fclsopni  23908  fclselbas  23909  ustssxp  24098  ustbasel  24100  ustincl  24101  ustdiag  24102  ustinvel  24103  ustexhalf  24104  ustfilxp  24106  ustbas2  24119  ustbas  24121  psmetf  24200  psmet0  24202  psmettri2  24203  metflem  24222  xmetf  24223  xmeteq0  24232  xmettri2  24234  tmsxms  24380  tmsms  24381  metustsym  24449  tngnrg  24568  cncff  24792  cncfi  24793  cfili  25174  iscmet3lem2  25198  mbfres  25551  mbfimaopnlem  25562  limcresi  25792  dvcnp2  25827  dvcnp2OLD  25828  ulmcl  26296  ulmf  26297  ulmcau  26310  pserulm  26337  pserdvlem2  26344  sinq34lt0t  26424  logtayl  26575  dchrmhm  27158  lgsdir2lem2  27243  2sqlem9  27344  mulog2sum  27454  newbdayim  27820  eleei  28830  uhgrf  28995  ushgrf  28996  upgrf  29019  umgrf  29031  uspgrf  29087  usgrf  29088  usgrfs  29090  nbcplgr  29367  clwlkcompim  29716  tncp  30413  eulplig  30420  grpofo  30434  grpolidinv  30436  grpoass  30438  nvvop  30544  phpar  30759  pjch1  31605  toslub  32905  tosglb  32907  chnub  32944  orngsqr  33288  exsslsb  33598  fldextsubrg  33651  fldextress  33653  zhmnrg  33961  issgon  34119  measfrge0  34199  measvnul  34202  measvun  34205  fzssfzo  34536  bnj916  34929  bnj983  34947  cplgredgex  35108  acycgrcycl  35134  mfsdisj  35537  mtyf2  35538  maxsta  35541  mvtinf  35542  r1peuqusdeg1  35630  hfun  36161  hfsn  36162  hfelhf  36164  hfuni  36167  hfpw  36168  fneuni  36330  curryset  36929  mptsnunlem  37321  heibor1lem  37798  heiborlem1  37800  heiborlem3  37802  opidonOLD  37841  isexid2  37844  elrelsrelim  38474  eqvrelqsel  38602  elpcliN  39882  lnrfg  43101  sdomne0  43395  sdomne0d  43396  pwinfi2  43544  frege55lem1c  43898  gneispacef  44117  gneispacef2  44118  gneispacern2  44121  gneispace0nelrn  44122  gneispaceel  44125  gneispacess  44127  mnuop123d  44244  trintALTVD  44862  trintALT  44863  eliuniin  45086  eliuniin2  45107  disjrnmpt2  45175  stoweidlem35  46026  saluncl  46308  saldifcl  46310  0sal  46311  sge0resplit  46397  omedm  46490  funressneu  47038  afvelrnb0  47155  afvelima  47158  rlimdmafv  47168  funressndmafv2rn  47214  rlimdmafv2  47249  elsetpreimafv  47376  oexpnegALTV  47668  gricbri  47906  grlimprop2  47975  grilcbri  47991  asslawass  48171  linindsi  48426  inisegn0a  48814  eloprab1st2nd  48846  uobrcl  49172  uobeq2  49380  isinito2  49478  basrestermcfolem  49550  discsnterm  49553  islmd  49644