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 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ibir  271  elab3gf  3646  elab3g  3647  elimhyp  4549  elimhyp2v  4550  elimhyp3v  4551  elimhyp4v  4552  elpwi  4565  elsni  4602  elpri  4609  eltpi  4650  snssi  4747  prssi  4782  snelpwi  5415  prelpwi  5418  elxpi  5673  releldmb  5926  relelrnb  5927  elrnmpt2d  5946  eloni  6359  limuni2  6413  funeu  6550  fneu  6635  fvelima2  6923  fvelima  6936  fvelimad  6938  eloprabi  8048  fo2ndf  8104  orderseqlem  8141  tfrlem9  8360  oeeulem  8575  elqsi  8751  qsel  8782  ecopovsym  8805  elpmi  8831  elmapi  8834  pmsspw  8863  brdomi  8944  en0  9003  en0r  9005  en1  9009  mapdom1  9118  rexdif1en  9133  ominf  9212  unblem2  9241  unfilem1  9253  fodomfir  9275  fiin  9370  brwdomi  9518  canthwdom  9529  brwdom3i  9533  unxpwdom  9539  scott0  9848  acni  10017  djuinf  10160  pwdjudom  10186  fin1ai  10265  fin2i  10267  fin4i  10270  ssfin3ds  10302  fin23lem17  10310  fin23lem38  10321  fin23lem39  10322  isfin32i  10337  fin34  10362  isfin7-2  10368  fin1a2lem13  10384  fin12  10385  gchi  10597  wuntr  10678  wununi  10679  wunpw  10680  wunpr  10682  wun0  10691  tskpwss  10725  tskpw  10726  tsken  10727  grutr  10766  grupw  10768  grupr  10770  gruurn  10771  ingru  10788  indpi  10880  eliooord  13420  fzrev3i  13607  fzne1  13620  elfzole1  13684  elfzolt2  13685  bcp1nk  14341  rere  15161  nn0abscl  15351  climcl  15538  rlimcl  15542  rlimdm  15590  o1res  15599  rlimdmo1  15657  climcau  15710  caucvgb  15719  fprodcnv  16025  cshws0  17149  restsspw  17472  mreiincl  17636  catidex  17718  catcocl  17729  catass  17730  homa1  18082  homahom2  18083  odulat  18479  dlatjmdi  18570  psrel  18613  psref2  18614  pstr2  18615  reldir  18643  dirdm  18644  dirref  18645  dirtr  18646  dirge  18647  chnub  18666  mgmcl  18689  submgmss  18751  submgmcl  18753  submgmmgm  18754  submss  18855  subm0cl  18857  submcl  18858  submmnd  18860  efmndbasf  18922  subgsubm  19203  symgbasf1o  19433  symginv  19460  psgneu  19564  odmulg  19614  frgpnabl  19933  dprdgrp  20065  dprdf  20066  abvfge0  20883  abveq0  20887  abvmul  20890  abvtri  20891  orngsqr  20935  lbsss  21164  lbssp  21166  lbsind  21167  domnchr  21639  cssi  21791  linds1  21917  linds2  21918  lindsind  21924  opsrtoslem2  22164  opsrso  22166  mdetunilem9  22734  uniopn  23011  iunopn  23012  inopn  23013  fiinopn  23015  eltpsg  23057  basis1  23064  basis2  23065  eltg4i  23074  lmff  23415  t1sep2  23483  cmpfii  23523  ptfinfin  23633  kqhmph  23933  fbasne0  23944  0nelfb  23945  fbsspw  23946  fbasssin  23950  ufli  24028  uffixfr  24037  elfm  24061  fclsopni  24129  fclselbas  24130  ustssxp  24319  ustbasel  24321  ustincl  24322  ustdiag  24323  ustinvel  24324  ustexhalf  24325  ustfilxp  24327  ustbas2  24339  ustbas  24341  psmetf  24420  psmet0  24422  psmettri2  24423  metflem  24442  xmetf  24443  xmeteq0  24452  xmettri2  24454  tmsxms  24600  tmsms  24601  metustsym  24669  tngnrg  24788  cncff  25009  cncfi  25010  cfili  25384  iscmet3lem2  25408  mbfres  25760  mbfimaopnlem  25771  limcresi  26001  dvcnp2  26036  ulmcl  26498  ulmf  26499  ulmcau  26512  pserulm  26539  pserdvlem2  26545  sinq34lt0t  26628  logtayl  26779  dchrmhm  27359  lgsdir2lem2  27444  2sqlem9  27545  mulog2sum  27655  newbdayim  28050  eleei  29152  uhgrf  29317  ushgrf  29318  upgrf  29341  umgrf  29353  uspgrf  29409  usgrf  29410  usgrfs  29412  nbcplgr  29689  clwlkcompim  30034  tncp  30735  eulplig  30742  grpofo  30756  grpolidinv  30758  grpoass  30760  nvvop  30866  phpar  31081  pjch1  31927  nn0mnfxrd  33004  toslub  33201  tosglb  33203  suppgsumssiun  33300  exsslsb  33899  fldextsubrg  33951  fldextress  33953  zhmnrg  34267  issgon  34425  measfrge0  34505  measvnul  34508  measvun  34511  fzssfzo  34841  bnj916  35233  bnj983  35251  cplgredgex  35479  acycgrcycl  35505  mfsdisj  35908  mtyf2  35909  maxsta  35912  mvtinf  35913  r1peuqusdeg1  36001  hfun  36536  hfsn  36537  hfelhf  36539  hfuni  36542  hfpw  36543  fneuni  36715  elttcirr  36899  curryset  37438  mptsnunlem  37839  heibor1lem  38315  heiborlem1  38317  heiborlem3  38319  opidonOLD  38358  isexid2  38361  elrelsrelim  38949  presucmap  39001  eqvrelqsel  39206  eldisjsim1  39440  elpcliN  40524  lnrfg  43703  sdomne0  43996  sdomne0d  43997  pwinfi2  44145  frege55lem1c  44499  gneispacef  44718  gneispacef2  44719  gneispacern2  44722  gneispace0nelrn  44723  gneispaceel  44726  gneispacess  44728  mnuop123d  44831  trintALTVD  45447  trintALT  45448  eliuniin  45676  eliuniin2  45697  disjrnmpt2  45765  stoweidlem35  46608  saluncl  46890  saldifcl  46892  0sal  46893  sge0resplit  46979  omedm  47072  funressneu  47640  afvelrnb0  47757  afvelima  47760  rlimdmafv  47770  funressndmafv2rn  47816  rlimdmafv2  47851  elsetpreimafv  47990  oexpnegALTV  48298  gricbri  48537  grlimprop2  48607  grilcbri  48630  asslawass  48814  linindsi  49079  inisegn0a  49466  eloprab1st2nd  49498  uobrcl  49823  uobeq2  50031  isinito2  50129  basrestermcfolem  50201  discsnterm  50204  islmd  50295