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  3651  elab3g  3652  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elpwi  4570  elsni  4606  elpri  4613  eltpi  4652  snssi  4772  prssi  4785  snelpwi  5403  prelpwi  5407  elxpi  5660  releldmb  5910  relelrnb  5911  elrnmpt2d  5930  eloni  6342  limuni2  6395  funeu  6541  fneu  6628  fvelima2  6913  fvelima  6926  fvelimad  6928  eloprabi  8042  fo2ndf  8100  orderseqlem  8136  tfrlem9  8353  oeeulem  8565  elqsi  8739  qsel  8769  ecopovsym  8792  elpmi  8819  elmapi  8822  pmsspw  8850  brdomi  8931  en0  8989  en0r  8991  en1  8995  mapdom1  9106  rexdif1en  9122  ominf  9205  ominfOLD  9206  unblem2  9240  unfilem1  9254  fodomfir  9279  fiin  9373  brwdomi  9521  canthwdom  9532  brwdom3i  9536  unxpwdom  9542  scott0  9839  acni  9998  djuinf  10142  pwdjudom  10168  fin1ai  10246  fin2i  10248  fin4i  10251  ssfin3ds  10283  fin23lem17  10291  fin23lem38  10302  fin23lem39  10303  isfin32i  10318  fin34  10343  isfin7-2  10349  fin1a2lem13  10365  fin12  10366  gchi  10577  wuntr  10658  wununi  10659  wunpw  10660  wunpr  10662  wun0  10671  tskpwss  10705  tskpw  10706  tsken  10707  grutr  10746  grupw  10748  grupr  10750  gruurn  10751  ingru  10768  indpi  10860  eliooord  13366  fzrev3i  13552  fzne1  13565  elfzole1  13628  elfzolt2  13629  bcp1nk  14282  rere  15088  nn0abscl  15278  climcl  15465  rlimcl  15469  rlimdm  15517  o1res  15526  rlimdmo1  15584  climcau  15637  caucvgb  15646  fprodcnv  15949  cshws0  17072  restsspw  17394  mreiincl  17557  catidex  17635  catcocl  17646  catass  17647  homa1  17999  homahom2  18000  odulat  18394  dlatjmdi  18485  psrel  18528  psref2  18529  pstr2  18530  reldir  18558  dirdm  18559  dirref  18560  dirtr  18561  dirge  18562  mgmcl  18570  submgmss  18632  submgmcl  18634  submgmmgm  18635  submss  18736  subm0cl  18738  submcl  18739  submmnd  18740  efmndbasf  18802  subgsubm  19080  symgbasf1o  19305  symginv  19332  psgneu  19436  odmulg  19486  frgpnabl  19805  dprdgrp  19937  dprdf  19938  abvfge0  20723  abveq0  20727  abvmul  20730  abvtri  20731  lbsss  20984  lbssp  20986  lbsind  20987  domnchr  21442  cssi  21593  linds1  21719  linds2  21720  lindsind  21726  opsrtoslem2  21963  opsrso  21965  mdetunilem9  22507  uniopn  22784  iunopn  22785  inopn  22786  fiinopn  22788  eltpsg  22830  basis1  22837  basis2  22838  eltg4i  22847  lmff  23188  t1sep2  23256  cmpfii  23296  ptfinfin  23406  kqhmph  23706  fbasne0  23717  0nelfb  23718  fbsspw  23719  fbasssin  23723  ufli  23801  uffixfr  23810  elfm  23834  fclsopni  23902  fclselbas  23903  ustssxp  24092  ustbasel  24094  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ustfilxp  24100  ustbas2  24113  ustbas  24115  psmetf  24194  psmet0  24196  psmettri2  24197  metflem  24216  xmetf  24217  xmeteq0  24226  xmettri2  24228  tmsxms  24374  tmsms  24375  metustsym  24443  tngnrg  24562  cncff  24786  cncfi  24787  cfili  25168  iscmet3lem2  25192  mbfres  25545  mbfimaopnlem  25556  limcresi  25786  dvcnp2  25821  dvcnp2OLD  25822  ulmcl  26290  ulmf  26291  ulmcau  26304  pserulm  26331  pserdvlem2  26338  sinq34lt0t  26418  logtayl  26569  dchrmhm  27152  lgsdir2lem2  27237  2sqlem9  27338  mulog2sum  27448  newbdayim  27814  eleei  28824  uhgrf  28989  ushgrf  28990  upgrf  29013  umgrf  29025  uspgrf  29081  usgrf  29082  usgrfs  29084  nbcplgr  29361  clwlkcompim  29710  tncp  30407  eulplig  30414  grpofo  30428  grpolidinv  30430  grpoass  30432  nvvop  30538  phpar  30753  pjch1  31599  toslub  32899  tosglb  32901  chnub  32938  orngsqr  33282  exsslsb  33592  fldextsubrg  33645  fldextress  33647  zhmnrg  33955  issgon  34113  measfrge0  34193  measvnul  34196  measvun  34199  fzssfzo  34530  bnj916  34923  bnj983  34941  cplgredgex  35108  acycgrcycl  35134  mfsdisj  35537  mtyf2  35538  maxsta  35541  mvtinf  35542  r1peuqusdeg1  35630  hfun  36166  hfsn  36167  hfelhf  36169  hfuni  36172  hfpw  36173  fneuni  36335  curryset  36934  mptsnunlem  37326  heibor1lem  37803  heiborlem1  37805  heiborlem3  37807  opidonOLD  37846  isexid2  37849  elrelsrelim  38479  eqvrelqsel  38607  elpcliN  39887  lnrfg  43108  sdomne0  43402  sdomne0d  43403  pwinfi2  43551  frege55lem1c  43905  gneispacef  44124  gneispacef2  44125  gneispacern2  44128  gneispace0nelrn  44129  gneispaceel  44132  gneispacess  44134  mnuop123d  44251  trintALTVD  44869  trintALT  44870  eliuniin  45093  eliuniin2  45114  disjrnmpt2  45182  stoweidlem35  46033  saluncl  46315  saldifcl  46317  0sal  46318  sge0resplit  46404  omedm  46497  funressneu  47048  afvelrnb0  47165  afvelima  47168  rlimdmafv  47178  funressndmafv2rn  47224  rlimdmafv2  47259  elsetpreimafv  47386  oexpnegALTV  47678  gricbri  47916  grlimprop2  47985  grilcbri  48001  asslawass  48181  linindsi  48436  inisegn0a  48824  eloprab1st2nd  48856  uobrcl  49182  uobeq2  49390  isinito2  49488  basrestermcfolem  49560  discsnterm  49563  islmd  49654