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

Theorem ibi 256
 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 ibi.1 . . 3 (𝜑 → (𝜑𝜓))
21biimpd 219 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 52 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  ibir  257  elimh  1066  elab3gf  3505  elimhyp  4283  elimhyp2v  4284  elimhyp3v  4285  elimhyp4v  4286  elpwi  4305  elsni  4331  elpri  4335  eltpi  4364  snssi  4472  prssi  4485  prelpwi  5043  elxpi  5270  releldmb  5498  relelrnb  5499  elpredim  5835  eloni  5876  limuni2  5929  funeu  6056  fneu  6135  fvelima  6390  eloprabi  7381  fo2ndf  7434  tfrlem9  7633  oeeulem  7834  elqsi  7951  qsel  7977  ecopovsym  8001  elpmi  8027  elmapi  8030  pmsspw  8043  brdomi  8119  undom  8203  mapdom1  8280  ominf  8327  unblem2  8368  unfilem1  8379  fiin  8483  brwdomi  8628  canthwdom  8639  brwdom3i  8643  unxpwdom  8649  scott0  8912  acni  9067  pwcdadom  9239  fin1ai  9316  fin2i  9318  fin4i  9321  ssfin3ds  9353  fin23lem17  9361  fin23lem38  9372  fin23lem39  9373  isfin32i  9388  fin34  9413  isfin7-2  9419  fin1a2lem13  9435  fin12  9436  gchi  9647  wuntr  9728  wununi  9729  wunpw  9730  wunpr  9732  wun0  9741  tskpwss  9775  tskpw  9776  tsken  9777  grutr  9816  grupw  9818  grupr  9820  gruurn  9821  ingru  9838  indpi  9930  eliooord  12437  fzrev3i  12613  elfzole1  12685  elfzolt2  12686  fz1fzo0m1  12723  bcp1nk  13307  rere  14069  nn0abscl  14259  climcl  14437  rlimcl  14441  rlimdm  14489  o1res  14498  rlimdmo1  14555  climcau  14608  caucvgb  14617  fprodcnv  14919  cshws0  16014  restsspw  16299  mreiincl  16463  catidex  16541  catcocl  16552  catass  16553  homa1  16893  homahom2  16894  odulat  17352  dlatjmdi  17404  psrel  17410  psref2  17411  pstr2  17412  reldir  17440  dirdm  17441  dirref  17442  dirtr  17443  dirge  17444  mgmcl  17452  submss  17557  subm0cl  17559  submcl  17560  submmnd  17561  subgsubm  17823  symgbasf1o  18009  symginv  18028  psgneu  18132  odmulg  18179  efgsp1  18356  efgsres  18357  frgpnabl  18484  dprdgrp  18611  dprdf  18612  abvfge0  19031  abveq0  19035  abvmul  19038  abvtri  19039  lbsss  19289  lbssp  19291  lbsind  19292  opsrtoslem2  19699  opsrso  19701  domnchr  20094  cssi  20244  linds1  20365  linds2  20366  lindsind  20372  mdetunilem9  20643  uniopn  20921  iunopn  20922  inopn  20923  fiinopn  20925  eltpsg  20967  basis1  20974  basis2  20975  eltg4i  20984  lmff  21325  t1sep2  21393  cmpfii  21432  ptfinfin  21542  kqhmph  21842  fbasne0  21853  0nelfb  21854  fbsspw  21855  fbasssin  21859  ufli  21937  uffixfr  21946  elfm  21970  fclsopni  22038  fclselbas  22039  ustssxp  22227  ustbasel  22229  ustincl  22230  ustdiag  22231  ustinvel  22232  ustexhalf  22233  ustfilxp  22235  ustbas2  22248  ustbas  22250  psmetf  22330  psmet0  22332  psmettri2  22333  metflem  22352  xmetf  22353  xmeteq0  22362  xmettri2  22364  tmsxms  22510  tmsms  22511  metustsym  22579  tngnrg  22697  cncff  22915  cncfi  22916  cfili  23284  iscmet3lem2  23308  mbfres  23630  mbfimaopnlem  23641  limcresi  23868  dvcnp2  23902  ulmcl  24354  ulmf  24355  ulmcau  24368  pserulm  24395  pserdvlem2  24401  sinq34lt0t  24481  logtayl  24626  dchrmhm  25186  lgsdir2lem2  25271  2sqlem9  25372  mulog2sum  25446  eleei  25997  uhgrf  26177  ushgrf  26178  upgrf  26201  umgrf  26213  uspgrf  26270  usgrf  26271  usgrfs  26273  nbcplgr  26564  clwlkcompim  26910  tncp  27666  eulplig  27673  grpofo  27687  grpolidinv  27689  grpoass  27691  nvvop  27798  phpar  28013  pjch1  28863  toslub  30002  tosglb  30004  orngsqr  30138  zhmnrg  30345  issgon  30520  measfrge0  30600  measvnul  30603  measvun  30606  fzssfzo  30947  bnj916  31335  bnj983  31353  mfsdisj  31779  mtyf2  31780  maxsta  31783  mvtinf  31784  orderseqlem  32083  hfun  32616  hfsn  32617  hfelhf  32619  hfuni  32622  hfpw  32623  fneuni  32673  bj-elid  33415  mptsnunlem  33515  heibor1lem  33933  heiborlem1  33935  heiborlem3  33937  opidonOLD  33976  isexid2  33979  elrelsrelim  34573  elpcliN  35694  lnrfg  38208  pwinfi2  38386  frege55lem1c  38729  gneispacef  38952  gneispacef2  38953  gneispacern2  38956  gneispace0nelrn  38957  gneispaceel  38960  gneispacess  38962  trintALTVD  39632  trintALT  39633  eliuniin  39794  eliuniin2  39818  disjrnmpt2  39889  fvelimad  39970  stoweidlem35  40763  saluncl  41048  saldifcl  41050  0sal  41051  sge0resplit  41134  omedm  41227  afvelrnb0  41758  afvelima  41761  rlimdmafv  41771  oexpnegALTV  42106  submgmss  42310  submgmcl  42312  submgmmgm  42313  asslawass  42347  linindsi  42754
 Copyright terms: Public domain W3C validator