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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ibir  268  elab3gf  3675  elab3g  3676  elimhyp  4594  elimhyp2v  4595  elimhyp3v  4596  elimhyp4v  4597  elpwi  4610  elsni  4646  elpri  4651  eltpi  4692  snssi  4812  prssi  4825  snelpwi  5444  prelpwi  5448  elxpi  5699  releldmb  5946  relelrnb  5947  elrnmpt2d  5963  eloni  6375  limuni2  6427  funeu  6574  fneu  6660  fvelima  6958  fvelimad  6960  eloprabi  8049  fo2ndf  8107  orderseqlem  8143  tfrlem9  8385  oeeulem  8601  elqsi  8764  qsel  8790  ecopovsym  8813  elpmi  8840  elmapi  8843  pmsspw  8871  brdomi  8954  brdomiOLD  8955  en0  9013  en0r  9016  en1  9021  undomOLD  9060  mapdom1  9142  rexdif1en  9158  ominf  9258  ominfOLD  9259  unblem2  9296  unfilem1  9310  fiin  9417  brwdomi  9563  canthwdom  9574  brwdom3i  9578  unxpwdom  9584  scott0  9881  acni  10040  djuinf  10183  pwdjudom  10211  fin1ai  10288  fin2i  10290  fin4i  10293  ssfin3ds  10325  fin23lem17  10333  fin23lem38  10344  fin23lem39  10345  isfin32i  10360  fin34  10385  isfin7-2  10391  fin1a2lem13  10407  fin12  10408  gchi  10619  wuntr  10700  wununi  10701  wunpw  10702  wunpr  10704  wun0  10713  tskpwss  10747  tskpw  10748  tsken  10749  grutr  10788  grupw  10790  grupr  10792  gruurn  10793  ingru  10810  indpi  10902  eliooord  13383  fzrev3i  13568  elfzole1  13640  elfzolt2  13641  bcp1nk  14277  rere  15069  nn0abscl  15259  climcl  15443  rlimcl  15447  rlimdm  15495  o1res  15504  rlimdmo1  15562  climcau  15617  caucvgb  15626  fprodcnv  15927  cshws0  17035  restsspw  17377  mreiincl  17540  catidex  17618  catcocl  17629  catass  17630  homa1  17987  homahom2  17988  odulat  18388  dlatjmdi  18479  psrel  18522  psref2  18523  pstr2  18524  reldir  18552  dirdm  18553  dirref  18554  dirtr  18555  dirge  18556  mgmcl  18564  submss  18690  subm0cl  18692  submcl  18693  submmnd  18694  efmndbasf  18756  subgsubm  19028  symgbasf1o  19242  symginv  19270  psgneu  19374  odmulg  19424  frgpnabl  19743  dprdgrp  19875  dprdf  19876  abvfge0  20430  abveq0  20434  abvmul  20437  abvtri  20438  lbsss  20688  lbssp  20690  lbsind  20691  domnchr  21084  cssi  21237  linds1  21365  linds2  21366  lindsind  21372  opsrtoslem2  21617  opsrso  21619  mdetunilem9  22122  uniopn  22399  iunopn  22400  inopn  22401  fiinopn  22403  eltpsg  22445  eltpsgOLD  22446  basis1  22453  basis2  22454  eltg4i  22463  lmff  22805  t1sep2  22873  cmpfii  22913  ptfinfin  23023  kqhmph  23323  fbasne0  23334  0nelfb  23335  fbsspw  23336  fbasssin  23340  ufli  23418  uffixfr  23427  elfm  23451  fclsopni  23519  fclselbas  23520  ustssxp  23709  ustbasel  23711  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  ustfilxp  23717  ustbas2  23730  ustbas  23732  psmetf  23812  psmet0  23814  psmettri2  23815  metflem  23834  xmetf  23835  xmeteq0  23844  xmettri2  23846  tmsxms  23995  tmsms  23996  metustsym  24064  tngnrg  24191  cncff  24409  cncfi  24410  cfili  24785  iscmet3lem2  24809  mbfres  25161  mbfimaopnlem  25172  limcresi  25402  dvcnp2  25437  ulmcl  25893  ulmf  25894  ulmcau  25907  pserulm  25934  pserdvlem2  25940  sinq34lt0t  26019  logtayl  26168  dchrmhm  26744  lgsdir2lem2  26829  2sqlem9  26930  mulog2sum  27040  eleei  28155  uhgrf  28322  ushgrf  28323  upgrf  28346  umgrf  28358  uspgrf  28414  usgrf  28415  usgrfs  28417  nbcplgr  28691  clwlkcompim  29037  tncp  29731  eulplig  29738  grpofo  29752  grpolidinv  29754  grpoass  29756  nvvop  29862  phpar  30077  pjch1  30923  fzne1  31999  toslub  32143  tosglb  32145  orngsqr  32422  fldextsubrg  32730  fldextress  32731  zhmnrg  32947  issgon  33121  measfrge0  33201  measvnul  33204  measvun  33207  fzssfzo  33550  bnj916  33944  bnj983  33962  cplgredgex  34111  acycgrcycl  34138  mfsdisj  34541  mtyf2  34542  maxsta  34545  mvtinf  34546  hfun  35150  hfsn  35151  hfelhf  35153  hfuni  35156  hfpw  35157  gg-dvcnp2  35174  fneuni  35232  curryset  35827  mptsnunlem  36219  heibor1lem  36677  heiborlem1  36679  heiborlem3  36681  opidonOLD  36720  isexid2  36723  elrelsrelim  37358  eqvrelqsel  37486  elpcliN  38764  lnrfg  41861  sdomne0  42164  sdomne0d  42165  pwinfi2  42313  frege55lem1c  42667  gneispacef  42886  gneispacef2  42887  gneispacern2  42890  gneispace0nelrn  42891  gneispaceel  42894  gneispacess  42896  mnuop123d  43021  trintALTVD  43641  trintALT  43642  eliuniin  43788  eliuniin2  43809  disjrnmpt2  43886  fvelima2  43964  stoweidlem35  44751  saluncl  45033  saldifcl  45035  0sal  45036  sge0resplit  45122  omedm  45215  funressneu  45757  afvelrnb0  45872  afvelima  45875  rlimdmafv  45885  funressndmafv2rn  45931  rlimdmafv2  45966  elsetpreimafv  46053  oexpnegALTV  46345  isisomgr  46492  submgmss  46562  submgmcl  46564  submgmmgm  46565  asslawass  46603  linindsi  47128