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  3641  elab3g  3642  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elpwi  4567  elsni  4601  elpri  4608  eltpi  4649  snssi  4746  prssi  4780  snelpwi  5417  prelpwi  5420  elxpi  5678  releldmb  5936  relelrnb  5937  elrnmpt2d  5956  eloni  6393  limuni2  6447  funeu  6588  fneu  6674  fvelima2  6963  fvelima  6976  fvelimad  6978  eloprabi  8102  fo2ndf  8162  orderseqlem  8204  tfrlem9  8424  oeeulem  8641  elqsi  8817  qsel  8848  ecopovsym  8871  elpmi  8897  elmapi  8900  pmsspw  8936  brdomi  9017  en0  9076  en0r  9078  en1  9082  mapdom1  9192  rexdif1en  9207  ominf  9286  unblem2  9316  unfilem1  9328  fodomfir  9350  fiin  9444  brwdomi  9592  canthwdom  9603  brwdom3i  9607  unxpwdom  9613  hfelhfOLD  9946  hfunOLD  9949  hfsnOLD  9951  hfuniOLD  9955  hfpwOLD  9957  scott0b  9967  scott0OLD  9968  acni  10154  djuinf  10297  pwdjudom  10323  fin1ai  10401  fin2i  10403  fin4i  10406  ssfin3ds  10438  fin23lem17  10446  fin23lem38  10457  fin23lem39  10458  isfin32i  10473  fin34  10498  isfin7-2  10504  fin1a2lem13  10520  fin12  10521  gchi  10739  wuntr  10820  wununi  10821  wunpw  10822  wunpr  10824  wun0  10833  tskpwss  10867  tskpw  10868  tsken  10869  grutr  10908  grupw  10910  grupr  10912  gruurn  10913  ingru  10930  indpi  11022  eliooord  13566  fzrev3i  13755  fzne1  13768  elfzole1  13832  elfzolt2  13833  bcp1nk  14491  rere  15321  nn0abscl  15511  climcl  15698  rlimcl  15702  rlimdm  15750  o1res  15759  rlimdmo1  15817  climcau  15870  caucvgb  15879  fprodcnv  16182  cshws0  17311  restsspw  17634  mreiincl  17798  catidex  17880  catcocl  17891  catass  17892  homa1  18244  homahom2  18245  odulat  18641  dlatjmdi  18732  psrel  18775  psref2  18776  pstr2  18777  reldir  18805  dirdm  18806  dirref  18807  dirtr  18808  dirge  18809  chnub  18828  mgmcl  18851  submgmss  18926  submgmcl  18928  submgmmgm  18929  submss  19036  subm0cl  19038  submcl  19039  submmnd  19041  efmndbasf  19103  subgsubm  19391  symgbasf1o  19622  symginv  19649  psgneu  19753  odmulg  19803  frgpnabl  20122  dprdgrp  20254  dprdf  20255  abvfge0  21104  abveq0  21108  abvmul  21111  abvtri  21112  orngsqr  21156  lbsss  21385  lbssp  21387  lbsind  21388  domnchr  21871  cssi  22023  linds1  22149  linds2  22150  lindsind  22156  opsrtoslem2  22398  opsrso  22400  mdetunilem9  22968  uniopn  23248  iunopn  23249  inopn  23250  fiinopn  23252  eltpsg  23294  basis1  23301  basis2  23302  eltg4i  23311  lmff  23652  t1sep2  23720  cmpfii  23760  ptfinfin  23871  kqhmph  24171  fbasne0  24182  0nelfb  24183  fbsspw  24184  fbasssin  24188  ufli  24266  uffixfr  24275  elfm  24299  fclsopni  24367  fclselbas  24368  ustssxp  24557  ustbasel  24559  ustincl  24560  ustdiag  24561  ustinvel  24562  ustexhalf  24563  ustfilxp  24565  ustbas2  24577  ustbas  24579  psmetf  24658  psmet0  24660  psmettri2  24661  metflem  24680  xmetf  24681  xmeteq0  24690  xmettri2  24692  tmsxms  24838  tmsms  24839  metustsym  24907  tngnrg  25026  cncff  25247  cncfi  25248  cfili  25622  iscmet3lem2  25646  mbfres  25998  mbfimaopnlem  26009  limcresi  26238  dvcnp2  26273  ulmcl  26741  ulmf  26742  ulmcau  26755  pserulm  26782  pserdvlem2  26788  sinq34lt0t  26871  logtayl  27021  dchrmhm  27601  lgsdir2lem2  27686  2sqlem9  27787  mulog2sum  27897  newbdayim  28322  eleei  29508  uhgrf  29673  ushgrf  29674  upgrf  29697  umgrf  29709  uspgrf  29768  usgrf  29769  usgrfs  29771  nbcplgr  30048  clwlkcompim  30400  acycgrcycl  30786  tncp  31113  eulplig  31120  grpofo  31134  grpolidinv  31136  grpoass  31138  nvvop  31244  phpar  31459  pjch1  32305  nn0mnfxrd  33416  toslub  33607  tosglb  33609  suppgsumssiun  33709  exsslsb  34312  fldextsubrg  34364  fldextress  34366  zhmnrg  34680  issgon  34838  measfrge0  34919  measvnul  34922  measvun  34925  fzssfzo  35254  bnj916  35646  bnj983  35664  elkarden  35936  cplgredgex  36075  mfsdisj  36495  mtyf2  36496  maxsta  36499  mvtinf  36500  r1peuqusdeg1  36588  fneuni  37326  elttcirr  37510  curryset  38050  mptsnunlem  38466  heibor1lem  38946  heiborlem1  38948  heiborlem3  38950  opidonOLD  38989  isexid2  38992  elrelsrelim  39578  presucmap  39630  eqvrelqsel  39835  eldisjsim1  40069  elpcliN  41153  lnrfg  44324  sdomne0  44617  sdomne0d  44618  pwinfi2  44766  frege55lem1c  45119  gneispacef  45338  gneispacef2  45339  gneispacern2  45342  gneispace0nelrn  45343  gneispaceel  45346  gneispacess  45348  mnuop123d  45449  trintALTVD  46064  trintALT  46065  hfstructstruct  46234  eliuniin  46329  eliuniin2  46350  disjrnmpt2  46418  stoweidlem35  47260  saluncl  47542  saldifcl  47544  0sal  47545  sge0resplit  47631  omedm  47724  funressneu  48332  afvelrnb0  48449  afvelima  48452  rlimdmafv  48462  funressndmafv2rn  48508  rlimdmafv2  48543  elsetpreimafv  48682  oexpnegALTV  48990  gricbri  49229  grlimprop2  49299  grilcbri  49322  asslawass  49505  linindsi  49774  inisegn0a  50162  eloprab1st2nd  50194  uobrcl  50524  uobeq2  50751  isinito2  50849  basrestermcfolem  50924  discsnterm  50927  islmd  51063