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

Theorem ibi 241
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  |-  ( ph  ->  ( ph  <->  ps )
)
Assertion
Ref Expression
ibi  |-  ( ph  ->  ps )

Proof of Theorem ibi
StepHypRef Expression
1 ibi.1 . . 3  |-  ( ph  ->  ( ph  <->  ps )
)
21biimpd 207 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 47 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  ibir  242  elimh  947  elab3gf  3116  elimhyp  3853  elimhyp2v  3854  elimhyp3v  3855  elimhyp4v  3856  elpwi  3874  elpr2  3901  elpri  3902  elsni  3907  eltpi  3925  snssi  4022  prssi  4034  eloni  4734  limuni2  4785  elxpi  4861  releldmb  5079  relelrnb  5080  funeu  5447  fneu  5520  fvelima  5748  eloprabi  6641  fo2ndf  6684  tfrlem9  6849  oeeulem  7045  elqsi  7159  qsel  7184  ecopovsym  7207  elpmi  7236  elmapi  7239  pmsspw  7252  brdomi  7326  undom  7404  mapdom1  7481  ominf  7530  unblem2  7570  unfilem1  7581  fiin  7677  brwdomi  7788  canthwdom  7799  brwdom3i  7803  unxpwdom  7809  scott0  8098  acni  8220  pwcdadom  8390  fin1ai  8467  fin2i  8469  fin4i  8472  ssfin3ds  8504  fin23lem17  8512  fin23lem38  8523  fin23lem39  8524  isfin32i  8539  fin34  8564  isfin7-2  8570  fin1a2lem13  8586  fin12  8587  gchi  8796  wuntr  8877  wununi  8878  wunpw  8879  wunpr  8881  wun0  8890  tskpwss  8924  tskpw  8925  tsken  8926  grutr  8965  grupw  8967  grupr  8969  gruurn  8970  ingru  8987  indpi  9081  eliooord  11360  fzrev3i  11528  elfzole1  11565  elfzolt2  11566  bcm1k  12096  bcp1nk  12098  rere  12616  nn0abscl  12806  climcl  12982  rlimcl  12986  rlimdm  13034  o1res  13043  rlimdmo1  13100  climcau  13153  caucvgb  13162  cshws0  14133  restsspw  14375  mreiincl  14539  catidex  14617  catcocl  14628  catass  14629  homa1  14910  homahom2  14911  odulat  15320  dlatjmdi  15372  psrel  15378  psref2  15379  pstr2  15380  reldir  15408  dirdm  15409  dirref  15410  dirtr  15411  dirge  15412  submss  15483  subm0cl  15485  submcl  15486  submmnd  15487  subgsubm  15708  symgbasf1o  15893  symgcl  15901  symginv  15912  symgsssg  15978  symgfisg  15979  symggen  15981  symggen2  15982  psgnunilem5  16005  psgneu  16017  odmulg  16062  efgsp1  16239  efgsres  16240  frgpnabl  16358  dprdgrp  16494  dprdf  16495  abvfge0  16912  abveq0  16916  abvmul  16919  abvtri  16920  lbsss  17163  lbssp  17165  lbsind  17166  opsrtoslem2  17571  opsrso  17573  domnchr  17968  psgnghm2  18016  cssi  18114  linds1  18244  linds2  18245  lindsind  18251  mdetunilem9  18431  uniopn  18515  iunopn  18516  inopn  18517  fiinopn  18519  eltpsg  18555  basis1  18560  basis2  18561  eltg4i  18570  lmff  18910  t1sep2  18978  cmpfii  19017  kqhmph  19397  fbasne0  19408  0nelfb  19409  fbsspw  19410  fbasssin  19414  ufli  19492  uffixfr  19501  elfm  19525  fclsopni  19593  fclselbas  19594  ustssxp  19784  ustbasel  19786  ustincl  19787  ustdiag  19788  ustinvel  19789  ustexhalf  19790  ustfilxp  19792  ustbas2  19805  ustbas  19807  psmetf  19887  psmet0  19889  psmettri2  19890  metflem  19908  xmetf  19909  xmeteq0  19918  xmettri2  19920  tmsxms  20066  tmsms  20067  metustsymOLD  20141  metustsym  20142  tngnrg  20260  cncff  20474  cncfi  20475  cfili  20784  iscmet3lem2  20808  mbfres  21127  mbfimaopnlem  21138  limcresi  21365  dvcnp2  21399  ulmcl  21851  ulmf  21852  ulmcau  21865  pserulm  21892  pserdvlem2  21898  sinq34lt0t  21976  logtayl  22110  dchrmhm  22585  lgsdir2lem2  22668  2sqlem9  22717  mulog2sum  22791  eleei  23148  uhgraf  23243  umgraf2  23256  uslgraf  23278  usgraf  23279  usgraf0  23281  tncp  23670  grpofo  23691  grpolidinv  23693  grpoass  23695  opidon  23814  isexid2  23817  nvvop  23992  phpar  24229  pjch1  25078  toslub  26134  tosglb  26136  orngsqr  26277  zhmnrg  26401  issgon  26571  measfrge0  26622  measvnul  26625  measvun  26628  fzssfzo  26939  fprodcnv  27499  elpredim  27642  orderseqlem  27718  hfun  28221  hfsn  28222  hfelhf  28224  hfuni  28227  hfpw  28228  fneuni  28553  ptfinfin  28575  heibor1lem  28713  heiborlem1  28715  heiborlem3  28717  lnrfg  29480  stoweidlem35  29835  afvelrnb0  30075  afvelima  30078  rlimdmafv  30088  clwwisshclww  30476  frisusgrapr  30588  linindsi  30986  trintALTVD  31621  trintALT  31622  bnj916  31931  bnj983  31949  bj-elimhyp  32101  elpcliN  33542
  Copyright terms: Public domain W3C validator