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

Theorem ibi 244
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 210 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 49 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  ibir  245  elimh  964  elab3gf  3223  elimhyp  3967  elimhyp2v  3968  elimhyp3v  3969  elimhyp4v  3970  elpwi  3988  elpri  4013  elsni  4021  eltpi  4041  snssi  4141  prssi  4153  elxpi  4866  releldmb  5085  relelrnb  5086  elpredim  5408  eloni  5449  limuni2  5500  funeu  5622  fneu  5695  fvelima  5930  eloprabi  6866  fo2ndf  6911  tfrlem9  7108  oeeulem  7307  elqsi  7422  qsel  7447  ecopovsym  7470  elpmi  7495  elmapi  7498  pmsspw  7511  brdomi  7585  undom  7663  mapdom1  7740  ominf  7787  unblem2  7827  unfilem1  7838  fiin  7939  brwdomi  8086  canthwdom  8097  brwdom3i  8101  unxpwdom  8107  scott0  8359  acni  8477  pwcdadom  8647  fin1ai  8724  fin2i  8726  fin4i  8729  ssfin3ds  8761  fin23lem17  8769  fin23lem38  8780  fin23lem39  8781  isfin32i  8796  fin34  8821  isfin7-2  8827  fin1a2lem13  8843  fin12  8844  gchi  9050  wuntr  9131  wununi  9132  wunpw  9133  wunpr  9135  wun0  9144  tskpwss  9178  tskpw  9179  tsken  9180  grutr  9219  grupw  9221  grupr  9223  gruurn  9224  ingru  9241  indpi  9333  eliooord  11695  fzrev3i  11863  elfzole1  11929  elfzolt2  11930  bcp1nk  12502  rere  13174  nn0abscl  13364  climcl  13551  rlimcl  13555  rlimdm  13603  o1res  13612  rlimdmo1  13669  climcau  13722  caucvgb  13734  fprodcnv  14025  cshws0  15060  restsspw  15318  mreiincl  15490  catidex  15568  catcocl  15579  catass  15580  homa1  15920  homahom2  15921  odulat  16379  dlatjmdi  16431  psrel  16437  psref2  16438  pstr2  16439  reldir  16467  dirdm  16468  dirref  16469  dirtr  16470  dirge  16471  mgmcl  16479  submss  16585  subm0cl  16587  submcl  16588  submmnd  16589  subgsubm  16827  symgbasf1o  17012  symginv  17031  psgneu  17135  odmulg  17195  efgsp1  17375  efgsres  17376  frgpnabl  17499  dprdgrp  17625  dprdf  17626  abvfge0  18038  abveq0  18042  abvmul  18045  abvtri  18046  lbsss  18288  lbssp  18290  lbsind  18291  opsrtoslem2  18696  opsrso  18698  domnchr  19090  cssi  19234  linds1  19355  linds2  19356  lindsind  19362  mdetunilem9  19632  uniopn  19914  iunopn  19915  inopn  19916  fiinopn  19918  eltpsg  19947  basis1  19952  basis2  19953  eltg4i  19962  lmff  20304  t1sep2  20372  cmpfii  20411  ptfinfin  20521  kqhmph  20821  fbasne0  20832  0nelfb  20833  fbsspw  20834  fbasssin  20838  ufli  20916  uffixfr  20925  elfm  20949  fclsopni  21017  fclselbas  21018  ustssxp  21206  ustbasel  21208  ustincl  21209  ustdiag  21210  ustinvel  21211  ustexhalf  21212  ustfilxp  21214  ustbas2  21227  ustbas  21229  psmetf  21309  psmet0  21311  psmettri2  21312  metflem  21330  xmetf  21331  xmeteq0  21340  xmettri2  21342  tmsxms  21488  tmsms  21489  metustsym  21557  tngnrg  21664  cncff  21912  cncfi  21913  cfili  22225  iscmet3lem2  22249  mbfres  22587  mbfimaopnlem  22598  limcresi  22827  dvcnp2  22861  ulmcl  23323  ulmf  23324  ulmcau  23337  pserulm  23364  pserdvlem2  23370  sinq34lt0t  23451  logtayl  23592  dchrmhm  24156  lgsdir2lem2  24239  2sqlem9  24288  mulog2sum  24362  eleei  24914  uhgraf  25013  ushgraf  25016  umgraf2  25031  uslgraf  25059  usgraf  25060  usgraf0  25062  clwwisshclww  25521  frisusgrapr  25705  tncp  25896  grpofo  25913  grpolidinv  25915  grpoass  25917  opidonOLD  26036  isexid2  26039  nvvop  26214  phpar  26451  pjch1  27309  fz1fzo0m1  28373  toslub  28424  tosglb  28426  tosglbOLD  28427  orngsqr  28563  zhmnrg  28767  issgon  28941  measfrge0  29021  measvnul  29024  measvun  29027  fzssfzo  29418  bnj916  29740  bnj983  29758  mfsdisj  30184  mtyf2  30185  maxsta  30188  mvtinf  30189  orderseqlem  30485  hfun  30938  hfsn  30939  hfelhf  30941  hfuni  30944  hfpw  30945  fneuni  30996  bj-elimhyp  31146  bj-elid  31591  mptsnunlem  31681  heibor1lem  32055  heiborlem1  32057  heiborlem3  32059  elpcliN  33377  lnrfg  35898  pwinfi2  36086  frege55lem1c  36370  trintALTVD  37138  trintALT  37139  disjrnmpt2  37313  stoweidlem35  37716  saluncl  37979  saldifcl  37981  sge0resplit  38036  afvelrnb0  38378  afvelima  38381  rlimdmafv  38391  uhgrf  38816  ushgrf  38817  umgrf2  38839  uslgrf  38870  usgrf  38871  usgrf0  38873  uhgfALTV  38952  submgmss  39064  submgmcl  39066  submgmmgm  39067  asslawass  39101  linindsi  39514
  Copyright terms: Public domain W3C validator