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

Theorem ibi 234
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 200 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 46 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  ibir  235  elimh  924  elab3gf  3089  elimhyp  3789  elimhyp2v  3790  elimhyp3v  3791  elimhyp4v  3792  elpwi  3809  elpr2  3835  elpri  3836  elsni  3840  eltpi  3854  snssi  3944  prssi  3956  eloni  4593  limuni2  4644  elxpi  4896  releldmb  5106  relelrnb  5107  funeu  5479  fneu  5551  fvelima  5780  eloprabi  6415  fo2ndf  6455  tfrlem9  6648  oeeulem  6846  elqsi  6960  qsel  6985  ecopovsym  7008  elpmi  7037  elmapi  7040  pmsspw  7050  brdomi  7121  undom  7198  mapdom1  7274  ominf  7323  unblem2  7362  unfilem1  7373  fiin  7429  brwdomi  7538  canthwdom  7549  brwdom3i  7553  unxpwdom  7559  scott0  7812  acni  7928  pwcdadom  8098  fin1ai  8175  fin2i  8177  fin4i  8180  ssfin3ds  8212  fin23lem17  8220  fin23lem38  8231  fin23lem39  8232  isfin32i  8247  fin34  8272  isfin7-2  8278  fin1a2lem13  8294  fin12  8295  gchi  8501  wuntr  8582  wununi  8583  wunpw  8584  wunpr  8586  wun0  8595  tskpwss  8629  tskpw  8630  tsken  8631  grutr  8670  grupw  8672  grupr  8674  gruurn  8675  ingru  8692  indpi  8786  eliooord  10972  fzrev3i  11114  elfzole1  11149  elfzolt2  11150  bcm1k  11608  bcp1nk  11610  rere  11929  nn0abscl  12119  climcl  12295  rlimcl  12299  rlimdm  12347  o1res  12356  rlimdmo1  12413  climcau  12466  caucvgb  12475  restsspw  13661  mreiincl  13823  catidex  13901  catcocl  13912  catass  13913  homa1  14194  homahom2  14195  odulat  14574  dlatjmdi  14625  psrel  14637  psref2  14638  pstr2  14639  reldir  14680  dirdm  14681  dirref  14682  dirtr  14683  dirge  14684  submss  14752  subm0cl  14754  submcl  14755  submmnd  14756  subgsubm  14964  symgcl  15103  symginv  15107  odmulg  15194  efgsp1  15371  efgsres  15372  frgpnabl  15488  dprdgrp  15565  dprdf  15566  abvfge0  15912  abveq0  15916  abvmul  15919  abvtri  15920  lbsss  16151  lbssp  16153  lbsind  16154  opsrtoslem2  16547  opsrso  16549  domnchr  16815  cssi  16913  uniopn  16972  iunopn  16973  inopn  16974  fiinopn  16976  eltpsg  17012  basis1  17017  basis2  17018  eltg4i  17027  lmff  17367  t1sep2  17435  cmpfii  17474  kqhmph  17853  fbasne0  17864  0nelfb  17865  fbsspw  17866  fbasssin  17870  ufli  17948  uffixfr  17957  elfm  17981  fclsopni  18049  fclselbas  18050  ustssxp  18236  ustbasel  18238  ustincl  18239  ustdiag  18240  ustinvel  18241  ustexhalf  18242  ustfilxp  18244  ustbas2  18257  ustbas  18259  psmetf  18339  psmet0  18341  psmettri2  18342  metflem  18360  xmetf  18361  xmeteq0  18370  xmettri2  18372  tmsxms  18518  tmsms  18519  metustsymOLD  18593  metustsym  18594  tngnrg  18712  cncff  18925  cncfi  18926  cfili  19223  iscmet3lem2  19247  mbfres  19538  mbfimaopnlem  19549  limcresi  19774  dvcnp2  19808  ulmcl  20299  ulmf  20300  ulmcau  20313  pserulm  20340  pserdvlem2  20346  sinq34lt0t  20419  logtayl  20553  dchrmhm  21027  lgsdir2lem2  21110  2sqlem9  21159  mulog2sum  21233  uhgraf  21341  umgraf2  21354  uslgraf  21376  usgraf  21377  usgraf0  21379  tncp  21768  grpofo  21789  grpolidinv  21791  grpoass  21793  opidon  21912  isexid2  21915  nvvop  22090  phpar  22327  pjch1  23174  adjval  23395  toslub  24193  tosglb  24194  ofldsqr  24242  zhmnrg  24353  issgon  24508  measfrge0  24559  measvnul  24562  measvun  24565  fprodcnv  25309  elpredim  25453  orderseqlem  25529  eleei  25838  hfun  26121  hfsn  26122  hfelhf  26124  hfuni  26127  hfpw  26128  fneuni  26358  ptfinfin  26380  heibor1lem  26520  heiborlem1  26522  heiborlem3  26524  linds1  27259  linds2  27260  lindsind  27266  lnrfg  27302  symgsssg  27387  symgfisg  27388  symggen  27390  symggen2  27391  psgnunilem5  27396  psgneu  27408  psgnghm2  27417  stoweidlem35  27762  afvelrnb0  28006  afvelima  28009  rlimdmafv  28019  frisusgrapr  28443  trintALTVD  29054  trintALT  29055  bnj916  29366  bnj983  29384  elpcliN  30752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator