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  954  elab3gf  3235  elimhyp  3981  elimhyp2v  3982  elimhyp3v  3983  elimhyp4v  3984  elpwi  4002  elpr2  4029  elpri  4030  elsni  4035  eltpi  4054  snssi  4155  prssi  4167  eloni  4874  limuni2  4925  elxpi  5001  releldmb  5223  relelrnb  5224  funeu  5598  fneu  5671  fvelima  5906  eloprabi  6843  fo2ndf  6888  tfrlem9  7052  oeeulem  7248  elqsi  7363  qsel  7388  ecopovsym  7411  elpmi  7435  elmapi  7438  pmsspw  7451  brdomi  7525  undom  7603  mapdom1  7680  ominf  7730  unblem2  7771  unfilem1  7782  fiin  7880  brwdomi  7992  canthwdom  8003  brwdom3i  8007  unxpwdom  8013  scott0  8302  acni  8424  pwcdadom  8594  fin1ai  8671  fin2i  8673  fin4i  8676  ssfin3ds  8708  fin23lem17  8716  fin23lem38  8727  fin23lem39  8728  isfin32i  8743  fin34  8768  isfin7-2  8774  fin1a2lem13  8790  fin12  8791  gchi  9000  wuntr  9081  wununi  9082  wunpw  9083  wunpr  9085  wun0  9094  tskpwss  9128  tskpw  9129  tsken  9130  grutr  9169  grupw  9171  grupr  9173  gruurn  9174  ingru  9191  indpi  9283  eliooord  11588  fzrev3i  11750  elfzole1  11810  elfzolt2  11811  bcp1nk  12369  rere  12929  nn0abscl  13119  climcl  13296  rlimcl  13300  rlimdm  13348  o1res  13357  rlimdmo1  13414  climcau  13467  caucvgb  13476  cshws0  14458  restsspw  14701  mreiincl  14865  catidex  14943  catcocl  14954  catass  14955  homa1  15233  homahom2  15234  odulat  15644  dlatjmdi  15696  psrel  15702  psref2  15703  pstr2  15704  reldir  15732  dirdm  15733  dirref  15734  dirtr  15735  dirge  15736  mgmcl  15744  submss  15850  subm0cl  15852  submcl  15853  submmnd  15854  subgsubm  16092  symgbasf1o  16277  symginv  16296  psgneu  16400  odmulg  16447  efgsp1  16624  efgsres  16625  frgpnabl  16748  dprdgrp  16907  dprdf  16908  abvfge0  17339  abveq0  17343  abvmul  17346  abvtri  17347  lbsss  17591  lbssp  17593  lbsind  17594  opsrtoslem2  18017  opsrso  18019  domnchr  18436  cssi  18582  linds1  18712  linds2  18713  lindsind  18719  mdetunilem9  18989  uniopn  19273  iunopn  19274  inopn  19275  fiinopn  19277  eltpsg  19313  basis1  19318  basis2  19319  eltg4i  19328  lmff  19668  t1sep2  19736  cmpfii  19775  ptfinfin  19886  kqhmph  20186  fbasne0  20197  0nelfb  20198  fbsspw  20199  fbasssin  20203  ufli  20281  uffixfr  20290  elfm  20314  fclsopni  20382  fclselbas  20383  ustssxp  20573  ustbasel  20575  ustincl  20576  ustdiag  20577  ustinvel  20578  ustexhalf  20579  ustfilxp  20581  ustbas2  20594  ustbas  20596  psmetf  20676  psmet0  20678  psmettri2  20679  metflem  20697  xmetf  20698  xmeteq0  20707  xmettri2  20709  tmsxms  20855  tmsms  20856  metustsymOLD  20930  metustsym  20931  tngnrg  21049  cncff  21263  cncfi  21264  cfili  21573  iscmet3lem2  21597  mbfres  21917  mbfimaopnlem  21928  limcresi  22155  dvcnp2  22189  ulmcl  22641  ulmf  22642  ulmcau  22655  pserulm  22682  pserdvlem2  22688  sinq34lt0t  22767  logtayl  22906  dchrmhm  23381  lgsdir2lem2  23464  2sqlem9  23513  mulog2sum  23587  eleei  24065  uhgraf  24164  ushgraf  24167  umgraf2  24182  uslgraf  24210  usgraf  24211  usgraf0  24213  clwwisshclww  24672  frisusgrapr  24856  tncp  25045  grpofo  25066  grpolidinv  25068  grpoass  25070  opidonOLD  25189  isexid2  25192  nvvop  25367  phpar  25604  pjch1  26453  toslub  27522  tosglb  27524  orngsqr  27660  zhmnrg  27814  issgon  27989  measfrge0  28040  measvnul  28043  measvun  28046  fzssfzo  28356  mfsdisj  28776  mtyf2  28777  maxsta  28780  mvtinf  28781  fprodcnv  29081  elpredim  29224  orderseqlem  29300  hfun  29803  hfsn  29804  hfelhf  29806  hfuni  29809  hfpw  29810  fneuni  30133  heibor1lem  30273  heiborlem1  30275  heiborlem3  30277  lnrfg  31036  stoweidlem35  31702  afvelrnb0  32083  afvelima  32086  rlimdmafv  32096  uhgf  32202  submgmss  32314  submgmcl  32316  submgmmgm  32317  asslawass  32350  linindsi  32758  trintALTVD  33388  trintALT  33389  bnj916  33698  bnj983  33716  bj-elimhyp  33873  bj-elid  34303  elpcliN  35319  pwinfi2  37412  frege55lem1c  37556
  Copyright terms: Public domain W3C validator