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

Theorem ibi 268
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 233 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  ibir  269  elimhOLD  1075  elab3gf  3676  elimhyp  4533  elimhyp2v  4534  elimhyp3v  4535  elimhyp4v  4536  elpwi  4554  elsni  4581  elpri  4586  eltpi  4624  snssi  4740  prssi  4753  prelpwi  5336  elxpi  5576  releldmb  5815  relelrnb  5816  elrnmpt2d  5833  elpredim  6158  eloni  6199  limuni2  6250  funeu  6377  fneu  6458  fvelima  6728  fvelimad  6729  eloprabi  7752  fo2ndf  7808  tfrlem9  8012  oeeulem  8217  elqsi  8340  qsel  8366  ecopovsym  8389  elpmi  8415  elmapi  8418  pmsspw  8431  brdomi  8509  undom  8594  mapdom1  8671  ominf  8719  unblem2  8760  unfilem1  8771  fiin  8875  brwdomi  9021  canthwdom  9032  brwdom3i  9036  unxpwdom  9042  scott0  9304  acni  9460  djuinf  9603  pwdjudom  9627  fin1ai  9704  fin2i  9706  fin4i  9709  ssfin3ds  9741  fin23lem17  9749  fin23lem38  9760  fin23lem39  9761  isfin32i  9776  fin34  9801  isfin7-2  9807  fin1a2lem13  9823  fin12  9824  gchi  10035  wuntr  10116  wununi  10117  wunpw  10118  wunpr  10120  wun0  10129  tskpwss  10163  tskpw  10164  tsken  10165  grutr  10204  grupw  10206  grupr  10208  gruurn  10209  ingru  10226  indpi  10318  eliooord  12786  fzrev3i  12964  elfzole1  13036  elfzolt2  13037  bcp1nk  13667  rere  14471  nn0abscl  14662  climcl  14846  rlimcl  14850  rlimdm  14898  o1res  14907  rlimdmo1  14964  climcau  15017  caucvgb  15026  fprodcnv  15327  cshws0  16425  restsspw  16695  mreiincl  16857  catidex  16935  catcocl  16946  catass  16947  homa1  17287  homahom2  17288  odulat  17745  dlatjmdi  17797  psrel  17803  psref2  17804  pstr2  17805  reldir  17833  dirdm  17834  dirref  17835  dirtr  17836  dirge  17837  mgmcl  17845  submss  17959  subm0cl  17961  submcl  17962  submmnd  17963  subgsubm  18231  symgbasf1o  18431  symginv  18450  psgneu  18554  odmulg  18603  frgpnabl  18915  dprdgrp  19047  dprdf  19048  abvfge0  19513  abveq0  19517  abvmul  19520  abvtri  19521  lbsss  19769  lbssp  19771  lbsind  19772  opsrtoslem2  20183  opsrso  20185  domnchr  20595  cssi  20744  linds1  20870  linds2  20871  lindsind  20877  mdetunilem9  21145  uniopn  21421  iunopn  21422  inopn  21423  fiinopn  21425  eltpsg  21467  basis1  21474  basis2  21475  eltg4i  21484  lmff  21825  t1sep2  21893  cmpfii  21933  ptfinfin  22043  kqhmph  22343  fbasne0  22354  0nelfb  22355  fbsspw  22356  fbasssin  22360  ufli  22438  uffixfr  22447  elfm  22471  fclsopni  22539  fclselbas  22540  ustssxp  22728  ustbasel  22730  ustincl  22731  ustdiag  22732  ustinvel  22733  ustexhalf  22734  ustfilxp  22736  ustbas2  22749  ustbas  22751  psmetf  22831  psmet0  22833  psmettri2  22834  metflem  22853  xmetf  22854  xmeteq0  22863  xmettri2  22865  tmsxms  23011  tmsms  23012  metustsym  23080  tngnrg  23198  cncff  23416  cncfi  23417  cfili  23786  iscmet3lem2  23810  mbfres  24160  mbfimaopnlem  24171  limcresi  24398  dvcnp2  24432  ulmcl  24884  ulmf  24885  ulmcau  24898  pserulm  24925  pserdvlem2  24931  sinq34lt0t  25010  logtayl  25156  dchrmhm  25731  lgsdir2lem2  25816  2sqlem9  25917  mulog2sum  26027  eleei  26597  uhgrf  26761  ushgrf  26762  upgrf  26785  umgrf  26797  uspgrf  26853  usgrf  26854  usgrfs  26856  nbcplgr  27130  clwlkcompim  27475  tncp  28169  eulplig  28176  grpofo  28190  grpolidinv  28192  grpoass  28194  nvvop  28300  phpar  28515  pjch1  29361  fzne1  30424  toslub  30569  tosglb  30571  orngsqr  30791  fldextsubrg  30927  fldextress  30928  zhmnrg  31094  issgon  31268  measfrge0  31348  measvnul  31351  measvun  31354  fzssfzo  31695  bnj916  32091  bnj983  32109  cplgredgex  32251  acycgrcycl  32278  mfsdisj  32681  mtyf2  32682  maxsta  32685  mvtinf  32686  orderseqlem  32978  hfun  33523  hfsn  33524  hfelhf  33526  hfuni  33529  hfpw  33530  fneuni  33579  curryset  34141  mptsnunlem  34488  heibor1lem  34955  heiborlem1  34957  heiborlem3  34959  opidonOLD  34998  isexid2  35001  elrelsrelim  35595  eqvrelqsel  35718  elpcliN  36896  lnrfg  39584  pwinfi2  39786  frege55lem1c  40127  gneispacef  40350  gneispacef2  40351  gneispacern2  40354  gneispace0nelrn  40355  gneispaceel  40358  gneispacess  40360  mnuop123d  40463  trintALTVD  41079  trintALT  41080  eliuniin  41230  eliuniin2  41252  disjrnmpt2  41314  fvelima2  41397  stoweidlem35  42186  saluncl  42468  saldifcl  42470  0sal  42471  sge0resplit  42554  omedm  42647  funressneu  43148  afvelrnb0  43229  afvelima  43232  rlimdmafv  43242  funressndmafv2rn  43288  rlimdmafv2  43323  oexpnegALTV  43674  isisomgr  43821  submgmss  43891  submgmcl  43893  submgmmgm  43894  asslawass  43932  linindsi  44334
  Copyright terms: Public domain W3C validator