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  3668  elab3g  3669  elimhyp  4571  elimhyp2v  4572  elimhyp3v  4573  elimhyp4v  4574  elpwi  4587  elsni  4623  elpri  4630  eltpi  4669  snssi  4789  prssi  4802  snelpwi  5423  prelpwi  5427  elxpi  5681  releldmb  5931  relelrnb  5932  elrnmpt2d  5951  eloni  6367  limuni2  6420  funeu  6566  fneu  6653  fvelima2  6936  fvelima  6949  fvelimad  6951  eloprabi  8067  fo2ndf  8125  orderseqlem  8161  tfrlem9  8404  oeeulem  8618  elqsi  8789  qsel  8815  ecopovsym  8838  elpmi  8865  elmapi  8868  pmsspw  8896  brdomi  8978  brdomiOLD  8979  en0  9037  en0r  9039  en1  9043  undomOLD  9079  mapdom1  9161  rexdif1en  9177  ominf  9271  ominfOLD  9272  unblem2  9306  unfilem1  9320  fodomfir  9345  fiin  9439  brwdomi  9587  canthwdom  9598  brwdom3i  9602  unxpwdom  9608  scott0  9905  acni  10064  djuinf  10208  pwdjudom  10234  fin1ai  10312  fin2i  10314  fin4i  10317  ssfin3ds  10349  fin23lem17  10357  fin23lem38  10368  fin23lem39  10369  isfin32i  10384  fin34  10409  isfin7-2  10415  fin1a2lem13  10431  fin12  10432  gchi  10643  wuntr  10724  wununi  10725  wunpw  10726  wunpr  10728  wun0  10737  tskpwss  10771  tskpw  10772  tsken  10773  grutr  10812  grupw  10814  grupr  10816  gruurn  10817  ingru  10834  indpi  10926  eliooord  13427  fzrev3i  13613  fzne1  13626  elfzole1  13689  elfzolt2  13690  bcp1nk  14340  rere  15146  nn0abscl  15336  climcl  15520  rlimcl  15524  rlimdm  15572  o1res  15581  rlimdmo1  15639  climcau  15692  caucvgb  15701  fprodcnv  16004  cshws0  17126  restsspw  17450  mreiincl  17613  catidex  17691  catcocl  17702  catass  17703  homa1  18055  homahom2  18056  odulat  18450  dlatjmdi  18541  psrel  18584  psref2  18585  pstr2  18586  reldir  18614  dirdm  18615  dirref  18616  dirtr  18617  dirge  18618  mgmcl  18626  submgmss  18688  submgmcl  18690  submgmmgm  18691  submss  18792  subm0cl  18794  submcl  18795  submmnd  18796  efmndbasf  18858  subgsubm  19136  symgbasf1o  19361  symginv  19388  psgneu  19492  odmulg  19542  frgpnabl  19861  dprdgrp  19993  dprdf  19994  abvfge0  20779  abveq0  20783  abvmul  20786  abvtri  20787  lbsss  21040  lbssp  21042  lbsind  21043  domnchr  21498  cssi  21649  linds1  21775  linds2  21776  lindsind  21782  opsrtoslem2  22019  opsrso  22021  mdetunilem9  22563  uniopn  22840  iunopn  22841  inopn  22842  fiinopn  22844  eltpsg  22886  basis1  22893  basis2  22894  eltg4i  22903  lmff  23244  t1sep2  23312  cmpfii  23352  ptfinfin  23462  kqhmph  23762  fbasne0  23773  0nelfb  23774  fbsspw  23775  fbasssin  23779  ufli  23857  uffixfr  23866  elfm  23890  fclsopni  23958  fclselbas  23959  ustssxp  24148  ustbasel  24150  ustincl  24151  ustdiag  24152  ustinvel  24153  ustexhalf  24154  ustfilxp  24156  ustbas2  24169  ustbas  24171  psmetf  24250  psmet0  24252  psmettri2  24253  metflem  24272  xmetf  24273  xmeteq0  24282  xmettri2  24284  tmsxms  24430  tmsms  24431  metustsym  24499  tngnrg  24618  cncff  24842  cncfi  24843  cfili  25225  iscmet3lem2  25249  mbfres  25602  mbfimaopnlem  25613  limcresi  25843  dvcnp2  25878  dvcnp2OLD  25879  ulmcl  26347  ulmf  26348  ulmcau  26361  pserulm  26388  pserdvlem2  26395  sinq34lt0t  26475  logtayl  26626  dchrmhm  27209  lgsdir2lem2  27294  2sqlem9  27395  mulog2sum  27505  newbdayim  27871  eleei  28881  uhgrf  29046  ushgrf  29047  upgrf  29070  umgrf  29082  uspgrf  29138  usgrf  29139  usgrfs  29141  nbcplgr  29418  clwlkcompim  29767  tncp  30464  eulplig  30471  grpofo  30485  grpolidinv  30487  grpoass  30489  nvvop  30595  phpar  30810  pjch1  31656  toslub  32958  tosglb  32960  chnub  32997  orngsqr  33331  exsslsb  33641  fldextsubrg  33696  fldextress  33698  zhmnrg  34001  issgon  34159  measfrge0  34239  measvnul  34242  measvun  34245  fzssfzo  34576  bnj916  34969  bnj983  34987  cplgredgex  35148  acycgrcycl  35174  mfsdisj  35577  mtyf2  35578  maxsta  35581  mvtinf  35582  r1peuqusdeg1  35670  hfun  36201  hfsn  36202  hfelhf  36204  hfuni  36207  hfpw  36208  fneuni  36370  curryset  36969  mptsnunlem  37361  heibor1lem  37838  heiborlem1  37840  heiborlem3  37842  opidonOLD  37881  isexid2  37884  elrelsrelim  38511  eqvrelqsel  38639  elpcliN  39917  lnrfg  43118  sdomne0  43412  sdomne0d  43413  pwinfi2  43561  frege55lem1c  43915  gneispacef  44134  gneispacef2  44135  gneispacern2  44138  gneispace0nelrn  44139  gneispaceel  44142  gneispacess  44144  mnuop123d  44261  trintALTVD  44879  trintALT  44880  eliuniin  45103  eliuniin2  45124  disjrnmpt2  45192  stoweidlem35  46044  saluncl  46326  saldifcl  46328  0sal  46329  sge0resplit  46415  omedm  46508  funressneu  47056  afvelrnb0  47173  afvelima  47176  rlimdmafv  47186  funressndmafv2rn  47232  rlimdmafv2  47267  elsetpreimafv  47379  oexpnegALTV  47671  gricbri  47909  grlimprop2  47978  grilcbri  47994  asslawass  48148  linindsi  48403  inisegn0a  48794  eloprab1st2nd  48823  isinito2  49364  basrestermcfolem  49428  discsnterm  49431  islmd  49515