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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ibir  268  elab3gf  3628  elab3g  3629  elimhyp  4542  elimhyp2v  4543  elimhyp3v  4544  elimhyp4v  4545  elpwi  4558  elsni  4594  elpri  4599  eltpi  4639  snssi  4759  prssi  4772  snelpwi  5392  prelpwi  5396  elxpi  5646  releldmb  5891  relelrnb  5892  elrnmpt2d  5908  eloni  6316  limuni2  6367  funeu  6513  fneu  6599  fvelima  6895  fvelimad  6896  eloprabi  7975  fo2ndf  8033  orderseqlem  8048  tfrlem9  8290  oeeulem  8507  elqsi  8634  qsel  8660  ecopovsym  8683  elpmi  8709  elmapi  8712  pmsspw  8740  brdomi  8823  brdomiOLD  8824  en0  8882  en0r  8885  en1  8890  undomOLD  8929  mapdom1  9011  rexdif1en  9027  ominf  9127  ominfOLD  9128  unblem2  9165  unfilem1  9179  fiin  9283  brwdomi  9429  canthwdom  9440  brwdom3i  9444  unxpwdom  9450  scott0  9747  acni  9906  djuinf  10049  pwdjudom  10077  fin1ai  10154  fin2i  10156  fin4i  10159  ssfin3ds  10191  fin23lem17  10199  fin23lem38  10210  fin23lem39  10211  isfin32i  10226  fin34  10251  isfin7-2  10257  fin1a2lem13  10273  fin12  10274  gchi  10485  wuntr  10566  wununi  10567  wunpw  10568  wunpr  10570  wun0  10579  tskpwss  10613  tskpw  10614  tsken  10615  grutr  10654  grupw  10656  grupr  10658  gruurn  10659  ingru  10676  indpi  10768  eliooord  13243  fzrev3i  13428  elfzole1  13500  elfzolt2  13501  bcp1nk  14136  rere  14932  nn0abscl  15123  climcl  15307  rlimcl  15311  rlimdm  15359  o1res  15368  rlimdmo1  15426  climcau  15481  caucvgb  15490  fprodcnv  15792  cshws0  16900  restsspw  17239  mreiincl  17402  catidex  17480  catcocl  17491  catass  17492  homa1  17849  homahom2  17850  odulat  18250  dlatjmdi  18341  psrel  18384  psref2  18385  pstr2  18386  reldir  18414  dirdm  18415  dirref  18416  dirtr  18417  dirge  18418  mgmcl  18426  submss  18545  subm0cl  18547  submcl  18548  submmnd  18549  efmndbasf  18610  subgsubm  18873  symgbasf1o  19078  symginv  19106  psgneu  19210  odmulg  19259  frgpnabl  19571  dprdgrp  19702  dprdf  19703  abvfge0  20187  abveq0  20191  abvmul  20194  abvtri  20195  lbsss  20444  lbssp  20446  lbsind  20447  domnchr  20841  cssi  20994  linds1  21122  linds2  21123  lindsind  21129  opsrtoslem2  21368  opsrso  21370  mdetunilem9  21874  uniopn  22151  iunopn  22152  inopn  22153  fiinopn  22155  eltpsg  22197  eltpsgOLD  22198  basis1  22205  basis2  22206  eltg4i  22215  lmff  22557  t1sep2  22625  cmpfii  22665  ptfinfin  22775  kqhmph  23075  fbasne0  23086  0nelfb  23087  fbsspw  23088  fbasssin  23092  ufli  23170  uffixfr  23179  elfm  23203  fclsopni  23271  fclselbas  23272  ustssxp  23461  ustbasel  23463  ustincl  23464  ustdiag  23465  ustinvel  23466  ustexhalf  23467  ustfilxp  23469  ustbas2  23482  ustbas  23484  psmetf  23564  psmet0  23566  psmettri2  23567  metflem  23586  xmetf  23587  xmeteq0  23596  xmettri2  23598  tmsxms  23747  tmsms  23748  metustsym  23816  tngnrg  23943  cncff  24161  cncfi  24162  cfili  24537  iscmet3lem2  24561  mbfres  24913  mbfimaopnlem  24924  limcresi  25154  dvcnp2  25189  ulmcl  25645  ulmf  25646  ulmcau  25659  pserulm  25686  pserdvlem2  25692  sinq34lt0t  25771  logtayl  25920  dchrmhm  26494  lgsdir2lem2  26579  2sqlem9  26680  mulog2sum  26790  eleei  27553  uhgrf  27720  ushgrf  27721  upgrf  27744  umgrf  27756  uspgrf  27812  usgrf  27813  usgrfs  27815  nbcplgr  28089  clwlkcompim  28435  tncp  29127  eulplig  29134  grpofo  29148  grpolidinv  29150  grpoass  29152  nvvop  29258  phpar  29473  pjch1  30319  fzne1  31394  toslub  31536  tosglb  31538  orngsqr  31801  fldextsubrg  32022  fldextress  32023  zhmnrg  32213  issgon  32387  measfrge0  32467  measvnul  32470  measvun  32473  fzssfzo  32816  bnj916  33210  bnj983  33228  cplgredgex  33379  acycgrcycl  33406  mfsdisj  33809  mtyf2  33810  maxsta  33813  mvtinf  33814  hfun  34617  hfsn  34618  hfelhf  34620  hfuni  34623  hfpw  34624  fneuni  34673  curryset  35271  mptsnunlem  35663  heibor1lem  36123  heiborlem1  36125  heiborlem3  36127  opidonOLD  36166  isexid2  36169  elrelsrelim  36806  eqvrelqsel  36934  elpcliN  38212  lnrfg  41258  sdomne0  41394  sdomne0d  41395  pwinfi2  41543  frege55lem1c  41897  gneispacef  42118  gneispacef2  42119  gneispacern2  42122  gneispace0nelrn  42123  gneispaceel  42126  gneispacess  42128  mnuop123d  42253  trintALTVD  42873  trintALT  42874  eliuniin  43021  eliuniin2  43042  disjrnmpt2  43105  fvelima2  43186  stoweidlem35  43964  saluncl  44246  saldifcl  44248  0sal  44249  sge0resplit  44333  omedm  44426  funressneu  44959  afvelrnb0  45074  afvelima  45077  rlimdmafv  45087  funressndmafv2rn  45133  rlimdmafv2  45168  elsetpreimafv  45255  oexpnegALTV  45547  isisomgr  45694  submgmss  45764  submgmcl  45766  submgmmgm  45767  asslawass  45805  linindsi  46206