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  940  elab3gf  3100  elimhyp  3836  elimhyp2v  3837  elimhyp3v  3838  elimhyp4v  3839  elpwi  3857  elpr2  3884  elpri  3885  elsni  3890  eltpi  3908  snssi  4005  prssi  4017  eloni  4716  limuni2  4767  elxpi  4843  releldmb  5061  relelrnb  5062  funeu  5430  fneu  5503  fvelima  5731  eloprabi  6625  fo2ndf  6668  tfrlem9  6830  oeeulem  7028  elqsi  7142  qsel  7167  ecopovsym  7190  elpmi  7219  elmapi  7222  pmsspw  7235  brdomi  7309  undom  7387  mapdom1  7464  ominf  7513  unblem2  7553  unfilem1  7564  fiin  7660  brwdomi  7771  canthwdom  7782  brwdom3i  7786  unxpwdom  7792  scott0  8081  acni  8203  pwcdadom  8373  fin1ai  8450  fin2i  8452  fin4i  8455  ssfin3ds  8487  fin23lem17  8495  fin23lem38  8506  fin23lem39  8507  isfin32i  8522  fin34  8547  isfin7-2  8553  fin1a2lem13  8569  fin12  8570  gchi  8778  wuntr  8859  wununi  8860  wunpw  8861  wunpr  8863  wun0  8872  tskpwss  8906  tskpw  8907  tsken  8908  grutr  8947  grupw  8949  grupr  8951  gruurn  8952  ingru  8969  indpi  9063  eliooord  11342  fzrev3i  11506  elfzole1  11543  elfzolt2  11544  bcm1k  12074  bcp1nk  12076  rere  12594  nn0abscl  12784  climcl  12960  rlimcl  12964  rlimdm  13012  o1res  13021  rlimdmo1  13078  climcau  13131  caucvgb  13140  cshws0  14110  restsspw  14352  mreiincl  14516  catidex  14594  catcocl  14605  catass  14606  homa1  14887  homahom2  14888  odulat  15297  dlatjmdi  15349  psrel  15355  psref2  15356  pstr2  15357  reldir  15385  dirdm  15386  dirref  15387  dirtr  15388  dirge  15389  submss  15459  subm0cl  15461  submcl  15462  submmnd  15463  subgsubm  15682  symgbasf1o  15867  symgcl  15875  symginv  15886  symgsssg  15952  symgfisg  15953  symggen  15955  symggen2  15956  psgnunilem5  15979  psgneu  15991  odmulg  16036  efgsp1  16213  efgsres  16214  frgpnabl  16332  dprdgrp  16462  dprdf  16463  abvfge0  16830  abveq0  16834  abvmul  16837  abvtri  16838  lbsss  17079  lbssp  17081  lbsind  17082  opsrtoslem2  17497  opsrso  17499  domnchr  17804  psgnghm2  17852  cssi  17950  linds1  18080  linds2  18081  lindsind  18087  mdetunilem9  18267  uniopn  18351  iunopn  18352  inopn  18353  fiinopn  18355  eltpsg  18391  basis1  18396  basis2  18397  eltg4i  18406  lmff  18746  t1sep2  18814  cmpfii  18853  kqhmph  19233  fbasne0  19244  0nelfb  19245  fbsspw  19246  fbasssin  19250  ufli  19328  uffixfr  19337  elfm  19361  fclsopni  19429  fclselbas  19430  ustssxp  19620  ustbasel  19622  ustincl  19623  ustdiag  19624  ustinvel  19625  ustexhalf  19626  ustfilxp  19628  ustbas2  19641  ustbas  19643  psmetf  19723  psmet0  19725  psmettri2  19726  metflem  19744  xmetf  19745  xmeteq0  19754  xmettri2  19756  tmsxms  19902  tmsms  19903  metustsymOLD  19977  metustsym  19978  tngnrg  20096  cncff  20310  cncfi  20311  cfili  20620  iscmet3lem2  20644  mbfres  20963  mbfimaopnlem  20974  limcresi  21201  dvcnp2  21235  ulmcl  21730  ulmf  21731  ulmcau  21744  pserulm  21771  pserdvlem2  21777  sinq34lt0t  21855  logtayl  21989  dchrmhm  22464  lgsdir2lem2  22547  2sqlem9  22596  mulog2sum  22670  eleei  22965  uhgraf  23060  umgraf2  23073  uslgraf  23095  usgraf  23096  usgraf0  23098  tncp  23487  grpofo  23508  grpolidinv  23510  grpoass  23512  opidon  23631  isexid2  23634  nvvop  23809  phpar  24046  pjch1  24895  toslub  25951  tosglb  25953  orngsqr  26124  zhmnrg  26249  issgon  26419  measfrge0  26470  measvnul  26473  measvun  26476  fzssfzo  26781  fprodcnv  27340  elpredim  27483  orderseqlem  27559  hfun  28062  hfsn  28063  hfelhf  28065  hfuni  28068  hfpw  28069  fneuni  28389  ptfinfin  28411  heibor1lem  28549  heiborlem1  28551  heiborlem3  28553  lnrfg  29317  stoweidlem35  29673  afvelrnb0  29913  afvelima  29916  rlimdmafv  29926  clwwisshclww  30314  frisusgrapr  30426  linindsi  30687  trintALTVD  31315  trintALT  31316  bnj916  31625  bnj983  31643  elpcliN  33107
  Copyright terms: Public domain W3C validator