Theorem ibi 256

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  ibir  257  elimh  1050  elab3gf  3388  elimhyp  4179  elimhyp2v  4180  elimhyp3v  4181  elimhyp4v  4182  elpwi  4201  elsni  4227  elpri  4230  eltpi  4261  snssi  4371  prssi  4385  prelpwi  4945  elxpi  5164  releldmb  5392  relelrnb  5393  elpredim  5730  eloni  5771  limuni2  5824  funeu  5951  fneu  6033  fvelima  6287  eloprabi  7277  fo2ndf  7329  tfrlem9  7526  oeeulem  7726  elqsi  7843  qsel  7869  ecopovsym  7892  elpmi  7918  elmapi  7921  pmsspw  7934  brdomi  8008  undom  8089  mapdom1  8166  ominf  8213  unblem2  8254  unfilem1  8265  fiin  8369  brwdomi  8514  canthwdom  8525  brwdom3i  8529  unxpwdom  8535  scott0  8787  acni  8906  pwcdadom  9076  fin1ai  9153  fin2i  9155  fin4i  9158  ssfin3ds  9190  fin23lem17  9198  fin23lem38  9209  fin23lem39  9210  isfin32i  9225  fin34  9250  isfin7-2  9256  fin1a2lem13  9272  fin12  9273  gchi  9484  wuntr  9565  wununi  9566  wunpw  9567  wunpr  9569  wun0  9578  tskpwss  9612  tskpw  9613  tsken  9614  grutr  9653  grupw  9655  grupr  9657  gruurn  9658  ingru  9675  indpi  9767  eliooord  12271  fzrev3i  12445  elfzole1  12517  elfzolt2  12518  fz1fzo0m1  12555  bcp1nk  13144  rere  13906  nn0abscl  14096  climcl  14274  rlimcl  14278  rlimdm  14326  o1res  14335  rlimdmo1  14392  climcau  14445  caucvgb  14454  fprodcnv  14757  cshws0  15855  restsspw  16139  mreiincl  16303  catidex  16382  catcocl  16393  catass  16394  homa1  16734  homahom2  16735  odulat  17192  dlatjmdi  17244  psrel  17250  psref2  17251  pstr2  17252  reldir  17280  dirdm  17281  dirref  17282  dirtr  17283  dirge  17284  mgmcl  17292  submss  17397  subm0cl  17399  submcl  17400  submmnd  17401  subgsubm  17663  symgbasf1o  17849  symginv  17868  psgneu  17972  odmulg  18019  efgsp1  18196  efgsres  18197  frgpnabl  18324  dprdgrp  18450  dprdf  18451  abvfge0  18870  abveq0  18874  abvmul  18877  abvtri  18878  lbsss  19125  lbssp  19127  lbsind  19128  opsrtoslem2  19533  opsrso  19535  domnchr  19928  cssi  20076  linds1  20197  linds2  20198  lindsind  20204  mdetunilem9  20474  uniopn  20750  iunopn  20751  inopn  20752  fiinopn  20754  eltpsg  20795  basis1  20802  basis2  20803  eltg4i  20812  lmff  21153  t1sep2  21221  cmpfii  21260  ptfinfin  21370  kqhmph  21670  fbasne0  21681  0nelfb  21682  fbsspw  21683  fbasssin  21687  ufli  21765  uffixfr  21774  elfm  21798  fclsopni  21866  fclselbas  21867  ustssxp  22055  ustbasel  22057  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  ustfilxp  22063  ustbas2  22076  ustbas  22078  psmetf  22158  psmet0  22160  psmettri2  22161  metflem  22180  xmetf  22181  xmeteq0  22190  xmettri2  22192  tmsxms  22338  tmsms  22339  metustsym  22407  tngnrg  22525  cncff  22743  cncfi  22744  cfili  23112  iscmet3lem2  23136  mbfres  23456  mbfimaopnlem  23467  limcresi  23694  dvcnp2  23728  ulmcl  24180  ulmf  24181  ulmcau  24194  pserulm  24221  pserdvlem2  24227  sinq34lt0t  24306  logtayl  24451  dchrmhm  25011  lgsdir2lem2  25096  2sqlem9  25197  mulog2sum  25271  eleei  25822  uhgrf  26002  ushgrf  26003  upgrf  26026  umgrf  26038  uspgrf  26094  usgrf  26095  usgrfs  26097  nbcplgr  26386  clwlkcompim  26732  tncp  27460  eulplig  27467  grpofo  27481  grpolidinv  27483  grpoass  27485  nvvop  27592  phpar  27807  pjch1  28657  toslub  29796  tosglb  29798  orngsqr  29932  zhmnrg  30139  issgon  30314  measfrge0  30394  measvnul  30397  measvun  30400  fzssfzo  30741  bnj916  31129  bnj983  31147  mfsdisj  31573  mtyf2  31574  maxsta  31577  mvtinf  31578  orderseqlem  31877  hfun  32410  hfsn  32411  hfelhf  32413  hfuni  32416  hfpw  32417  fneuni  32467  bj-elid  33215  mptsnunlem  33315  heibor1lem  33738  heiborlem1  33740  heiborlem3  33742  opidonOLD  33781  isexid2  33784  elrelsrelim  34378  elpcliN  35497  lnrfg  38006  pwinfi2  38184  frege55lem1c  38527  gneispacef  38750  gneispacef2  38751  gneispacern2  38754  gneispace0nelrn  38755  gneispaceel  38758  gneispacess  38760  trintALTVD  39430  trintALT  39431  eliuniin  39593  eliuniin2  39617  disjrnmpt2  39689  fvelimad  39772  stoweidlem35  40570  saluncl  40855  saldifcl  40857  0sal  40858  sge0resplit  40941  omedm  41034  afvelrnb0  41565  afvelima  41568  rlimdmafv  41578  submgmss  42117  submgmcl  42119  submgmmgm  42120  asslawass  42154  linindsi  42561