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  3628  elab3g  3629  elimhyp  4533  elimhyp2v  4534  elimhyp3v  4535  elimhyp4v  4536  elpwi  4549  elsni  4585  elpri  4592  eltpi  4633  snssi  4752  prssi  4765  snelpwi  5391  prelpwi  5394  elxpi  5646  releldmb  5895  relelrnb  5896  elrnmpt2d  5915  eloni  6327  limuni2  6380  funeu  6517  fneu  6602  fvelima2  6886  fvelima  6899  fvelimad  6901  eloprabi  8009  fo2ndf  8064  orderseqlem  8100  tfrlem9  8317  oeeulem  8530  elqsi  8705  qsel  8736  ecopovsym  8759  elpmi  8786  elmapi  8789  pmsspw  8818  brdomi  8899  en0  8958  en0r  8960  en1  8964  mapdom1  9073  rexdif1en  9088  ominf  9167  unblem2  9196  unfilem1  9208  fodomfir  9231  fiin  9328  brwdomi  9476  canthwdom  9487  brwdom3i  9491  unxpwdom  9497  scott0  9801  acni  9958  djuinf  10102  pwdjudom  10128  fin1ai  10206  fin2i  10208  fin4i  10211  ssfin3ds  10243  fin23lem17  10251  fin23lem38  10262  fin23lem39  10263  isfin32i  10278  fin34  10303  isfin7-2  10309  fin1a2lem13  10325  fin12  10326  gchi  10538  wuntr  10619  wununi  10620  wunpw  10621  wunpr  10623  wun0  10632  tskpwss  10666  tskpw  10667  tsken  10668  grutr  10707  grupw  10709  grupr  10711  gruurn  10712  ingru  10729  indpi  10821  eliooord  13349  fzrev3i  13536  fzne1  13549  elfzole1  13613  elfzolt2  13614  bcp1nk  14270  rere  15075  nn0abscl  15265  climcl  15452  rlimcl  15456  rlimdm  15504  o1res  15513  rlimdmo1  15571  climcau  15624  caucvgb  15633  fprodcnv  15939  cshws0  17063  restsspw  17385  mreiincl  17549  catidex  17631  catcocl  17642  catass  17643  homa1  17995  homahom2  17996  odulat  18392  dlatjmdi  18483  psrel  18526  psref2  18527  pstr2  18528  reldir  18556  dirdm  18557  dirref  18558  dirtr  18559  dirge  18560  chnub  18579  mgmcl  18602  submgmss  18664  submgmcl  18666  submgmmgm  18667  submss  18768  subm0cl  18770  submcl  18771  submmnd  18772  efmndbasf  18834  subgsubm  19115  symgbasf1o  19341  symginv  19368  psgneu  19472  odmulg  19522  frgpnabl  19841  dprdgrp  19973  dprdf  19974  abvfge0  20782  abveq0  20786  abvmul  20789  abvtri  20790  orngsqr  20834  lbsss  21064  lbssp  21066  lbsind  21067  domnchr  21522  cssi  21674  linds1  21800  linds2  21801  lindsind  21807  opsrtoslem2  22044  opsrso  22046  mdetunilem9  22595  uniopn  22872  iunopn  22873  inopn  22874  fiinopn  22876  eltpsg  22918  basis1  22925  basis2  22926  eltg4i  22935  lmff  23276  t1sep2  23344  cmpfii  23384  ptfinfin  23494  kqhmph  23794  fbasne0  23805  0nelfb  23806  fbsspw  23807  fbasssin  23811  ufli  23889  uffixfr  23898  elfm  23922  fclsopni  23990  fclselbas  23991  ustssxp  24180  ustbasel  24182  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  ustfilxp  24188  ustbas2  24200  ustbas  24202  psmetf  24281  psmet0  24283  psmettri2  24284  metflem  24303  xmetf  24304  xmeteq0  24313  xmettri2  24315  tmsxms  24461  tmsms  24462  metustsym  24530  tngnrg  24649  cncff  24870  cncfi  24871  cfili  25245  iscmet3lem2  25269  mbfres  25621  mbfimaopnlem  25632  limcresi  25862  dvcnp2  25897  ulmcl  26359  ulmf  26360  ulmcau  26373  pserulm  26400  pserdvlem2  26406  sinq34lt0t  26486  logtayl  26637  dchrmhm  27218  lgsdir2lem2  27303  2sqlem9  27404  mulog2sum  27514  newbdayim  27909  eleei  28980  uhgrf  29145  ushgrf  29146  upgrf  29169  umgrf  29181  uspgrf  29237  usgrf  29238  usgrfs  29240  nbcplgr  29517  clwlkcompim  29863  tncp  30564  eulplig  30571  grpofo  30585  grpolidinv  30587  grpoass  30589  nvvop  30695  phpar  30910  pjch1  31756  nn0mnfxrd  32839  toslub  33048  tosglb  33050  suppgsumssiun  33148  exsslsb  33756  fldextsubrg  33809  fldextress  33811  zhmnrg  34125  issgon  34283  measfrge0  34363  measvnul  34366  measvun  34369  fzssfzo  34699  bnj916  35091  bnj983  35109  cplgredgex  35319  acycgrcycl  35345  mfsdisj  35748  mtyf2  35749  maxsta  35752  mvtinf  35753  r1peuqusdeg1  35841  hfun  36376  hfsn  36377  hfelhf  36379  hfuni  36382  hfpw  36383  fneuni  36545  elttcirr  36729  curryset  37269  mptsnunlem  37668  heibor1lem  38144  heiborlem1  38146  heiborlem3  38148  opidonOLD  38187  isexid2  38190  elrelsrelim  38778  presucmap  38830  eqvrelqsel  39035  eldisjsim1  39269  elpcliN  40353  lnrfg  43565  sdomne0  43858  sdomne0d  43859  pwinfi2  44007  frege55lem1c  44361  gneispacef  44580  gneispacef2  44581  gneispacern2  44584  gneispace0nelrn  44585  gneispaceel  44588  gneispacess  44590  mnuop123d  44707  trintALTVD  45324  trintALT  45325  eliuniin  45547  eliuniin2  45568  disjrnmpt2  45636  stoweidlem35  46481  saluncl  46763  saldifcl  46765  0sal  46766  sge0resplit  46852  omedm  46945  funressneu  47507  afvelrnb0  47624  afvelima  47627  rlimdmafv  47637  funressndmafv2rn  47683  rlimdmafv2  47718  elsetpreimafv  47857  oexpnegALTV  48165  gricbri  48404  grlimprop2  48474  grilcbri  48497  asslawass  48681  linindsi  48935  inisegn0a  49323  eloprab1st2nd  49355  uobrcl  49680  uobeq2  49888  isinito2  49986  basrestermcfolem  50058  discsnterm  50061  islmd  50152