Theorem ibi 270

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		ibi.1	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	1, 2	mpbid 235	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ibir  271  elab3gf  3637  elab3g  3638  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elpwi  4563  elsni  4597  elpri  4604  eltpi  4645  snssi  4742  prssi  4776  snelpwi  5411  prelpwi  5414  elxpi  5672  releldmb  5927  relelrnb  5928  elrnmpt2d  5947  eloni  6372  limuni2  6426  funeu  6565  fneu  6649  fvelima2  6937  fvelima  6950  fvelimad  6952  eloprabi  8074  fo2ndf  8134  orderseqlem  8176  tfrlem9  8396  oeeulem  8613  elqsi  8789  qsel  8820  ecopovsym  8843  elpmi  8869  elmapi  8872  pmsspw  8908  brdomi  8989  en0  9048  en0r  9050  en1  9054  mapdom1  9164  rexdif1en  9179  ominf  9258  unblem2  9288  unfilem1  9300  fodomfir  9322  fiin  9417  brwdomi  9565  canthwdom  9576  brwdom3i  9580  unxpwdom  9586  hfelhfOLD  9919  hfunOLD  9922  hfsnOLD  9924  hfuniOLD  9928  hfpwOLD  9930  scott0b  9940  scott0OLD  9941  acni  10127  djuinf  10270  pwdjudom  10296  fin1ai  10374  fin2i  10376  fin4i  10379  ssfin3ds  10411  fin23lem17  10419  fin23lem38  10430  fin23lem39  10431  isfin32i  10446  fin34  10471  isfin7-2  10477  fin1a2lem13  10493  fin12  10494  gchi  10712  wuntr  10793  wununi  10794  wunpw  10795  wunpr  10797  wun0  10806  tskpwss  10840  tskpw  10841  tsken  10842  grutr  10881  grupw  10883  grupr  10885  gruurn  10886  ingru  10903  indpi  10995  eliooord  13539  fzrev3i  13728  fzne1  13741  elfzole1  13805  elfzolt2  13806  bcp1nk  14464  rere  15294  nn0abscl  15484  climcl  15671  rlimcl  15675  rlimdm  15723  o1res  15732  rlimdmo1  15790  climcau  15843  caucvgb  15852  fprodcnv  16155  cshws0  17284  restsspw  17607  mreiincl  17771  catidex  17853  catcocl  17864  catass  17865  homa1  18217  homahom2  18218  odulat  18614  dlatjmdi  18705  psrel  18748  psref2  18749  pstr2  18750  reldir  18778  dirdm  18779  dirref  18780  dirtr  18781  dirge  18782  chnub  18801  mgmcl  18824  submgmss  18899  submgmcl  18901  submgmmgm  18902  submss  19009  subm0cl  19011  submcl  19012  submmnd  19014  efmndbasf  19076  subgsubm  19364  symgbasf1o  19594  symginv  19621  psgneu  19725  odmulg  19775  frgpnabl  20094  dprdgrp  20226  dprdf  20227  abvfge0  21076  abveq0  21080  abvmul  21083  abvtri  21084  orngsqr  21128  lbsss  21357  lbssp  21359  lbsind  21360  domnchr  21843  cssi  21995  linds1  22121  linds2  22122  lindsind  22128  opsrtoslem2  22370  opsrso  22372  mdetunilem9  22940  uniopn  23220  iunopn  23221  inopn  23222  fiinopn  23224  eltpsg  23266  basis1  23273  basis2  23274  eltg4i  23283  lmff  23624  t1sep2  23692  cmpfii  23732  ptfinfin  23843  kqhmph  24143  fbasne0  24154  0nelfb  24155  fbsspw  24156  fbasssin  24160  ufli  24238  uffixfr  24247  elfm  24271  fclsopni  24339  fclselbas  24340  ustssxp  24529  ustbasel  24531  ustincl  24532  ustdiag  24533  ustinvel  24534  ustexhalf  24535  ustfilxp  24537  ustbas2  24549  ustbas  24551  psmetf  24630  psmet0  24632  psmettri2  24633  metflem  24652  xmetf  24653  xmeteq0  24662  xmettri2  24664  tmsxms  24810  tmsms  24811  metustsym  24879  tngnrg  24998  cncff  25219  cncfi  25220  cfili  25594  iscmet3lem2  25618  mbfres  25970  mbfimaopnlem  25981  limcresi  26210  dvcnp2  26245  ulmcl  26713  ulmf  26714  ulmcau  26727  pserulm  26754  pserdvlem2  26760  sinq34lt0t  26843  logtayl  26993  dchrmhm  27573  lgsdir2lem2  27658  2sqlem9  27759  mulog2sum  27869  newbdayim  28294  eleei  29480  uhgrf  29645  ushgrf  29646  upgrf  29669  umgrf  29681  uspgrf  29740  usgrf  29741  usgrfs  29743  nbcplgr  30020  clwlkcompim  30372  acycgrcycl  30758  tncp  31085  eulplig  31092  grpofo  31106  grpolidinv  31108  grpoass  31110  nvvop  31216  phpar  31431  pjch1  32277  nn0mnfxrd  33389  toslub  33580  tosglb  33582  suppgsumssiun  33679  exsslsb  34275  fldextsubrg  34327  fldextress  34329  zhmnrg  34643  issgon  34801  measfrge0  34882  measvnul  34885  measvun  34888  fzssfzo  35217  bnj916  35609  bnj983  35627  elkarden  35879  cplgredgex  35981  mfsdisj  36401  mtyf2  36402  maxsta  36405  mvtinf  36406  r1peuqusdeg1  36494  fneuni  37227  elttcirr  37411  curryset  37951  mptsnunlem  38354  heibor1lem  38836  heiborlem1  38838  heiborlem3  38840  opidonOLD  38879  isexid2  38882  elrelsrelim  39468  presucmap  39520  eqvrelqsel  39725  eldisjsim1  39959  elpcliN  41043  lnrfg  44214  sdomne0  44507  sdomne0d  44508  pwinfi2  44656  frege55lem1c  45009  gneispacef  45228  gneispacef2  45229  gneispacern2  45232  gneispace0nelrn  45233  gneispaceel  45236  gneispacess  45238  mnuop123d  45339  trintALTVD  45955  trintALT  45956  hfstructstruct  46118  eliuniin  46207  eliuniin2  46228  disjrnmpt2  46296  stoweidlem35  47138  saluncl  47420  saldifcl  47422  0sal  47423  sge0resplit  47509  omedm  47602  funressneu  48210  afvelrnb0  48327  afvelima  48330  rlimdmafv  48340  funressndmafv2rn  48386  rlimdmafv2  48421  elsetpreimafv  48560  oexpnegALTV  48868  gricbri  49107  grlimprop2  49177  grilcbri  49200  asslawass  49383  linindsi  49652  inisegn0a  50040  eloprab1st2nd  50072  uobrcl  50402  uobeq2  50629  isinito2  50727  basrestermcfolem  50802  discsnterm  50805  islmd  50941