Theorem ibi 258

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 220	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 52	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  ibir  259  elimh  1096  elab3gf  3562  elimhyp  4353  elimhyp2v  4354  elimhyp3v  4355  elimhyp4v  4356  elpwi  4372  elsni  4398  elpri  4403  eltpi  4432  snssi  4540  prssi  4553  prelpwi  5118  elxpi  5345  releldmb  5574  relelrnb  5575  elpredim  5918  eloni  5959  limuni2  6011  funeu  6135  fneu  6215  fvelima  6478  eloprabi  7474  fo2ndf  7527  tfrlem9  7726  oeeulem  7927  elqsi  8044  qsel  8070  ecopovsym  8094  elpmi  8120  elmapi  8123  pmsspw  8136  brdomi  8212  undom  8296  mapdom1  8373  ominf  8420  unblem2  8461  unfilem1  8472  fiin  8576  brwdomi  8721  canthwdom  8732  brwdom3i  8736  unxpwdom  8742  scott0  9005  acni  9160  pwcdadom  9332  fin1ai  9409  fin2i  9411  fin4i  9414  ssfin3ds  9446  fin23lem17  9454  fin23lem38  9465  fin23lem39  9466  isfin32i  9481  fin34  9506  isfin7-2  9512  fin1a2lem13  9528  fin12  9529  gchi  9740  wuntr  9821  wununi  9822  wunpw  9823  wunpr  9825  wun0  9834  tskpwss  9868  tskpw  9869  tsken  9870  grutr  9909  grupw  9911  grupr  9913  gruurn  9914  ingru  9931  indpi  10023  eliooord  12470  fzrev3i  12649  elfzole1  12721  elfzolt2  12722  fz1fzo0m1  12759  bcp1nk  13343  rere  14104  nn0abscl  14294  climcl  14472  rlimcl  14476  rlimdm  14524  o1res  14533  rlimdmo1  14590  climcau  14643  caucvgb  14652  fprodcnv  14953  cshws0  16039  restsspw  16316  mreiincl  16480  catidex  16558  catcocl  16569  catass  16570  homa1  16910  homahom2  16911  odulat  17369  dlatjmdi  17421  psrel  17427  psref2  17428  pstr2  17429  reldir  17457  dirdm  17458  dirref  17459  dirtr  17460  dirge  17461  mgmcl  17469  submss  17574  subm0cl  17576  submcl  17577  submmnd  17578  subgsubm  17837  symgbasf1o  18023  symginv  18042  psgneu  18146  odmulg  18193  efgsp1  18370  efgsres  18371  frgpnabl  18498  dprdgrp  18625  dprdf  18626  abvfge0  19045  abveq0  19049  abvmul  19052  abvtri  19053  lbsss  19303  lbssp  19305  lbsind  19306  opsrtoslem2  19712  opsrso  19714  domnchr  20107  cssi  20258  linds1  20379  linds2  20380  lindsind  20386  mdetunilem9  20657  uniopn  20935  iunopn  20936  inopn  20937  fiinopn  20939  eltpsg  20981  basis1  20988  basis2  20989  eltg4i  20998  lmff  21339  t1sep2  21407  cmpfii  21446  ptfinfin  21556  kqhmph  21856  fbasne0  21867  0nelfb  21868  fbsspw  21869  fbasssin  21873  ufli  21951  uffixfr  21960  elfm  21984  fclsopni  22052  fclselbas  22053  ustssxp  22241  ustbasel  22243  ustincl  22244  ustdiag  22245  ustinvel  22246  ustexhalf  22247  ustfilxp  22249  ustbas2  22262  ustbas  22264  psmetf  22344  psmet0  22346  psmettri2  22347  metflem  22366  xmetf  22367  xmeteq0  22376  xmettri2  22378  tmsxms  22524  tmsms  22525  metustsym  22593  tngnrg  22711  cncff  22929  cncfi  22930  cfili  23299  iscmet3lem2  23323  mbfres  23647  mbfimaopnlem  23658  limcresi  23885  dvcnp2  23919  ulmcl  24371  ulmf  24372  ulmcau  24385  pserulm  24412  pserdvlem2  24418  sinq34lt0t  24498  logtayl  24642  dchrmhm  25202  lgsdir2lem2  25287  2sqlem9  25388  mulog2sum  25462  eleei  26013  uhgrf  26193  ushgrf  26194  upgrf  26217  umgrf  26229  uspgrf  26286  usgrf  26287  usgrfs  26289  nbcplgr  26580  clwlkcompim  26926  tncp  27683  eulplig  27690  grpofo  27704  grpolidinv  27706  grpoass  27708  nvvop  27814  phpar  28029  pjch1  28879  toslub  30015  tosglb  30017  orngsqr  30151  zhmnrg  30358  issgon  30533  measfrge0  30613  measvnul  30616  measvun  30619  fzssfzo  30960  bnj916  31347  bnj983  31365  mfsdisj  31791  mtyf2  31792  maxsta  31795  mvtinf  31796  orderseqlem  32094  hfun  32627  hfsn  32628  hfelhf  32630  hfuni  32633  hfpw  32634  fneuni  32684  bj-elid  33419  mptsnunlem  33520  heibor1lem  33937  heiborlem1  33939  heiborlem3  33941  opidonOLD  33980  isexid2  33983  elrelsrelim  34569  elpcliN  35691  lnrfg  38207  pwinfi2  38384  frege55lem1c  38727  gneispacef  38950  gneispacef2  38951  gneispacern2  38954  gneispace0nelrn  38955  gneispaceel  38958  gneispacess  38960  trintALTVD  39627  trintALT  39628  eliuniin  39789  eliuniin2  39812  disjrnmpt2  39881  fvelimad  39959  stoweidlem35  40748  saluncl  41033  saldifcl  41035  0sal  41036  sge0resplit  41119  omedm  41212  funressneu  41683  afvelrnb0  41770  afvelima  41773  rlimdmafv  41783  funressndmafv2rn  41829  rlimdmafv2  41864  oexpnegALTV  42180  submgmss  42377  submgmcl  42379  submgmmgm  42380  asslawass  42414  linindsi  42821