MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ibi Structured version   Visualization version   GIF version

Theorem ibi 266
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
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 ibi.1 . 2 (𝜑 → (𝜑𝜓))
31, 2mpbid 231 1 (𝜑𝜓)
Colors of variables: wff setvar class
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  267  elab3gf  3634  elab3g  3635  elimhyp  4549  elimhyp2v  4550  elimhyp3v  4551  elimhyp4v  4552  elpwi  4565  elsni  4601  elpri  4606  eltpi  4646  snssi  4766  prssi  4779  snelpwi  5398  prelpwi  5402  elxpi  5653  releldmb  5899  relelrnb  5900  elrnmpt2d  5916  eloni  6325  limuni2  6377  funeu  6523  fneu  6609  fvelima  6905  fvelimad  6906  eloprabi  7991  fo2ndf  8049  orderseqlem  8085  tfrlem9  8327  oeeulem  8544  elqsi  8705  qsel  8731  ecopovsym  8754  elpmi  8780  elmapi  8783  pmsspw  8811  brdomi  8894  brdomiOLD  8895  en0  8953  en0r  8956  en1  8961  undomOLD  9000  mapdom1  9082  rexdif1en  9098  ominf  9198  ominfOLD  9199  unblem2  9236  unfilem1  9250  fiin  9354  brwdomi  9500  canthwdom  9511  brwdom3i  9515  unxpwdom  9521  scott0  9818  acni  9977  djuinf  10120  pwdjudom  10148  fin1ai  10225  fin2i  10227  fin4i  10230  ssfin3ds  10262  fin23lem17  10270  fin23lem38  10281  fin23lem39  10282  isfin32i  10297  fin34  10322  isfin7-2  10328  fin1a2lem13  10344  fin12  10345  gchi  10556  wuntr  10637  wununi  10638  wunpw  10639  wunpr  10641  wun0  10650  tskpwss  10684  tskpw  10685  tsken  10686  grutr  10725  grupw  10727  grupr  10729  gruurn  10730  ingru  10747  indpi  10839  eliooord  13315  fzrev3i  13500  elfzole1  13572  elfzolt2  13573  bcp1nk  14209  rere  14999  nn0abscl  15189  climcl  15373  rlimcl  15377  rlimdm  15425  o1res  15434  rlimdmo1  15492  climcau  15547  caucvgb  15556  fprodcnv  15858  cshws0  16966  restsspw  17305  mreiincl  17468  catidex  17546  catcocl  17557  catass  17558  homa1  17915  homahom2  17916  odulat  18316  dlatjmdi  18407  psrel  18450  psref2  18451  pstr2  18452  reldir  18480  dirdm  18481  dirref  18482  dirtr  18483  dirge  18484  mgmcl  18492  submss  18612  subm0cl  18614  submcl  18615  submmnd  18616  efmndbasf  18677  subgsubm  18941  symgbasf1o  19147  symginv  19175  psgneu  19279  odmulg  19329  frgpnabl  19644  dprdgrp  19775  dprdf  19776  abvfge0  20266  abveq0  20270  abvmul  20273  abvtri  20274  lbsss  20523  lbssp  20525  lbsind  20526  domnchr  20920  cssi  21073  linds1  21201  linds2  21202  lindsind  21208  opsrtoslem2  21447  opsrso  21449  mdetunilem9  21953  uniopn  22230  iunopn  22231  inopn  22232  fiinopn  22234  eltpsg  22276  eltpsgOLD  22277  basis1  22284  basis2  22285  eltg4i  22294  lmff  22636  t1sep2  22704  cmpfii  22744  ptfinfin  22854  kqhmph  23154  fbasne0  23165  0nelfb  23166  fbsspw  23167  fbasssin  23171  ufli  23249  uffixfr  23258  elfm  23282  fclsopni  23350  fclselbas  23351  ustssxp  23540  ustbasel  23542  ustincl  23543  ustdiag  23544  ustinvel  23545  ustexhalf  23546  ustfilxp  23548  ustbas2  23561  ustbas  23563  psmetf  23643  psmet0  23645  psmettri2  23646  metflem  23665  xmetf  23666  xmeteq0  23675  xmettri2  23677  tmsxms  23826  tmsms  23827  metustsym  23895  tngnrg  24022  cncff  24240  cncfi  24241  cfili  24616  iscmet3lem2  24640  mbfres  24992  mbfimaopnlem  25003  limcresi  25233  dvcnp2  25268  ulmcl  25724  ulmf  25725  ulmcau  25738  pserulm  25765  pserdvlem2  25771  sinq34lt0t  25850  logtayl  25999  dchrmhm  26573  lgsdir2lem2  26658  2sqlem9  26759  mulog2sum  26869  eleei  27732  uhgrf  27899  ushgrf  27900  upgrf  27923  umgrf  27935  uspgrf  27991  usgrf  27992  usgrfs  27994  nbcplgr  28268  clwlkcompim  28614  tncp  29306  eulplig  29313  grpofo  29327  grpolidinv  29329  grpoass  29331  nvvop  29437  phpar  29652  pjch1  30498  fzne1  31574  toslub  31716  tosglb  31718  orngsqr  31982  fldextsubrg  32217  fldextress  32218  zhmnrg  32417  issgon  32591  measfrge0  32671  measvnul  32674  measvun  32677  fzssfzo  33020  bnj916  33414  bnj983  33432  cplgredgex  33583  acycgrcycl  33610  mfsdisj  34013  mtyf2  34014  maxsta  34017  mvtinf  34018  hfun  34730  hfsn  34731  hfelhf  34733  hfuni  34736  hfpw  34737  fneuni  34786  curryset  35384  mptsnunlem  35776  heibor1lem  36235  heiborlem1  36237  heiborlem3  36239  opidonOLD  36278  isexid2  36281  elrelsrelim  36917  eqvrelqsel  37045  elpcliN  38323  lnrfg  41384  sdomne0  41627  sdomne0d  41628  pwinfi2  41776  frege55lem1c  42130  gneispacef  42349  gneispacef2  42350  gneispacern2  42353  gneispace0nelrn  42354  gneispaceel  42357  gneispacess  42359  mnuop123d  42484  trintALTVD  43104  trintALT  43105  eliuniin  43251  eliuniin2  43272  disjrnmpt2  43343  fvelima2  43424  stoweidlem35  44208  saluncl  44490  saldifcl  44492  0sal  44493  sge0resplit  44579  omedm  44672  funressneu  45213  afvelrnb0  45328  afvelima  45331  rlimdmafv  45341  funressndmafv2rn  45387  rlimdmafv2  45422  elsetpreimafv  45509  oexpnegALTV  45801  isisomgr  45948  submgmss  46018  submgmcl  46020  submgmmgm  46021  asslawass  46059  linindsi  46460
  Copyright terms: Public domain W3C validator