Theorem ibi 255

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		ibi.1	. . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
2	1	biimpd 218	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 50	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  ibir  256  elimh  1024  elimhOLD  1027  elab3gf  3325  elimhyp  4096  elimhyp2v  4097  elimhyp3v  4098  elimhyp4v  4099  elpwi  4117  elsni  4142  elpri  4145  eltpi  4176  snssi  4280  prssi  4293  prelpwi  4842  elxpi  5054  releldmb  5281  relelrnb  5282  elpredim  5609  eloni  5650  limuni2  5703  funeu  5828  fneu  5909  fvelima  6158  eloprabi  7121  fo2ndf  7171  tfrlem9  7368  oeeulem  7568  elqsi  7687  qsel  7713  ecopovsym  7736  elpmi  7762  elmapi  7765  pmsspw  7778  brdomi  7852  undom  7933  mapdom1  8010  ominf  8057  unblem2  8098  unfilem1  8109  fiin  8211  brwdomi  8356  canthwdom  8367  brwdom3i  8371  unxpwdom  8377  scott0  8632  acni  8751  pwcdadom  8921  fin1ai  8998  fin2i  9000  fin4i  9003  ssfin3ds  9035  fin23lem17  9043  fin23lem38  9054  fin23lem39  9055  isfin32i  9070  fin34  9095  isfin7-2  9101  fin1a2lem13  9117  fin12  9118  gchi  9325  wuntr  9406  wununi  9407  wunpw  9408  wunpr  9410  wun0  9419  tskpwss  9453  tskpw  9454  tsken  9455  grutr  9494  grupw  9496  grupr  9498  gruurn  9499  ingru  9516  indpi  9608  eliooord  12104  fzrev3i  12277  elfzole1  12347  elfzolt2  12348  fz1fzo0m1  12383  bcp1nk  12966  rere  13710  nn0abscl  13900  climcl  14078  rlimcl  14082  rlimdm  14130  o1res  14139  rlimdmo1  14196  climcau  14249  caucvgb  14258  fprodcnv  14552  cshws0  15646  restsspw  15915  mreiincl  16079  catidex  16158  catcocl  16169  catass  16170  homa1  16510  homahom2  16511  odulat  16968  dlatjmdi  17020  psrel  17026  psref2  17027  pstr2  17028  reldir  17056  dirdm  17057  dirref  17058  dirtr  17059  dirge  17060  mgmcl  17068  submss  17173  subm0cl  17175  submcl  17176  submmnd  17177  subgsubm  17439  symgbasf1o  17626  symginv  17645  psgneu  17749  odmulg  17796  efgsp1  17973  efgsres  17974  frgpnabl  18101  dprdgrp  18227  dprdf  18228  abvfge0  18645  abveq0  18649  abvmul  18652  abvtri  18653  lbsss  18898  lbssp  18900  lbsind  18901  opsrtoslem2  19306  opsrso  19308  domnchr  19699  cssi  19847  linds1  19968  linds2  19969  lindsind  19975  mdetunilem9  20245  uniopn  20527  iunopn  20528  inopn  20529  fiinopn  20531  eltpsg  20560  basis1  20565  basis2  20566  eltg4i  20575  lmff  20915  t1sep2  20983  cmpfii  21022  ptfinfin  21132  kqhmph  21432  fbasne0  21444  0nelfb  21445  fbsspw  21446  fbasssin  21450  ufli  21528  uffixfr  21537  elfm  21561  fclsopni  21629  fclselbas  21630  ustssxp  21818  ustbasel  21820  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ustfilxp  21826  ustbas2  21839  ustbas  21841  psmetf  21921  psmet0  21923  psmettri2  21924  metflem  21943  xmetf  21944  xmeteq0  21953  xmettri2  21955  tmsxms  22101  tmsms  22102  metustsym  22170  tngnrg  22288  cncff  22504  cncfi  22505  cfili  22874  iscmet3lem2  22898  mbfres  23217  mbfimaopnlem  23228  limcresi  23455  dvcnp2  23489  ulmcl  23939  ulmf  23940  ulmcau  23953  pserulm  23980  pserdvlem2  23986  sinq34lt0t  24065  logtayl  24206  dchrmhm  24766  lgsdir2lem2  24851  2sqlem9  24952  mulog2sum  25026  eleei  25577  uhgrf  25728  ushgrf  25729  upgrf  25753  umgrf  25764  uhgraf  25828  ushgraf  25831  umgraf2  25846  uslgraf  25874  usgraf  25875  usgraf0  25877  clwwisshclww  26335  frisusgrapr  26518  tncp  26721  grpofo  26737  grpolidinv  26739  grpoass  26741  nvvop  26848  phpar  27063  pjch1  27913  toslub  28999  tosglb  29001  orngsqr  29135  zhmnrg  29339  issgon  29513  measfrge0  29593  measvnul  29596  measvun  29599  fzssfzo  29940  bnj916  30257  bnj983  30275  mfsdisj  30701  mtyf2  30702  maxsta  30705  mvtinf  30706  orderseqlem  30993  hfun  31455  hfsn  31456  hfelhf  31458  hfuni  31461  hfpw  31462  fneuni  31512  bj-elid  32262  mptsnunlem  32361  heibor1lem  32778  heiborlem1  32780  heiborlem3  32782  opidonOLD  32821  isexid2  32824  elpcliN  34197  lnrfg  36708  pwinfi2  36886  frege55lem1c  37230  gneispacef  37453  gneispacef2  37454  gneispacern2  37457  gneispace0nelrn  37458  gneispaceel  37461  gneispacess  37463  trintALTVD  38138  trintALT  38139  disjrnmpt2  38370  stoweidlem35  38928  saluncl  39213  saldifcl  39215  sge0resplit  39299  afvelrnb0  39893  afvelima  39896  rlimdmafv  39906  uspgrf  40384  usgrf  40385  usgrfs  40387  nbcplgr  40656  clWlkcompim  40987  crctcsh1wlkn0  41024  submgmss  41582  submgmcl  41584  submgmmgm  41585  asslawass  41619  linindsi  42030