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  3255  elimhyp  3998  elimhyp2v  3999  elimhyp3v  4000  elimhyp4v  4001  elpwi  4019  elpr2  4046  elpri  4047  elsni  4052  eltpi  4071  snssi  4171  prssi  4183  eloni  4888  limuni2  4939  elxpi  5015  releldmb  5235  relelrnb  5236  funeu  5610  fneu  5683  fvelima  5917  eloprabi  6843  fo2ndf  6887  tfrlem9  7051  oeeulem  7247  elqsi  7362  qsel  7387  ecopovsym  7410  elpmi  7434  elmapi  7437  pmsspw  7450  brdomi  7524  undom  7602  mapdom1  7679  ominf  7729  unblem2  7769  unfilem1  7780  fiin  7878  brwdomi  7990  canthwdom  8001  brwdom3i  8005  unxpwdom  8011  scott0  8300  acni  8422  pwcdadom  8592  fin1ai  8669  fin2i  8671  fin4i  8674  ssfin3ds  8706  fin23lem17  8714  fin23lem38  8725  fin23lem39  8726  isfin32i  8741  fin34  8766  isfin7-2  8772  fin1a2lem13  8788  fin12  8789  gchi  8998  wuntr  9079  wununi  9080  wunpw  9081  wunpr  9083  wun0  9092  tskpwss  9126  tskpw  9127  tsken  9128  grutr  9167  grupw  9169  grupr  9171  gruurn  9172  ingru  9189  indpi  9281  eliooord  11580  fzrev3i  11742  elfzole1  11800  elfzolt2  11801  bcm1k  12357  bcp1nk  12359  rere  12914  nn0abscl  13104  climcl  13281  rlimcl  13285  rlimdm  13333  o1res  13342  rlimdmo1  13399  climcau  13452  caucvgb  13461  cshws0  14440  restsspw  14683  mreiincl  14847  catidex  14925  catcocl  14936  catass  14937  homa1  15218  homahom2  15219  odulat  15628  dlatjmdi  15680  psrel  15686  psref2  15687  pstr2  15688  reldir  15716  dirdm  15717  dirref  15718  dirtr  15719  dirge  15720  submss  15791  subm0cl  15793  submcl  15794  submmnd  15795  subgsubm  16018  symgbasf1o  16203  symgcl  16211  symginv  16222  symgsssg  16288  symgfisg  16289  symggen  16291  symggen2  16292  psgnunilem5  16315  psgneu  16327  odmulg  16374  efgsp1  16551  efgsres  16552  frgpnabl  16670  dprdgrp  16829  dprdf  16830  abvfge0  17254  abveq0  17258  abvmul  17261  abvtri  17262  lbsss  17506  lbssp  17508  lbsind  17509  opsrtoslem2  17920  opsrso  17922  domnchr  18336  psgnghm2  18384  cssi  18482  linds1  18612  linds2  18613  lindsind  18619  mdetunilem9  18889  uniopn  19173  iunopn  19174  inopn  19175  fiinopn  19177  eltpsg  19213  basis1  19218  basis2  19219  eltg4i  19228  lmff  19568  t1sep2  19636  cmpfii  19675  kqhmph  20055  fbasne0  20066  0nelfb  20067  fbsspw  20068  fbasssin  20072  ufli  20150  uffixfr  20159  elfm  20183  fclsopni  20251  fclselbas  20252  ustssxp  20442  ustbasel  20444  ustincl  20445  ustdiag  20446  ustinvel  20447  ustexhalf  20448  ustfilxp  20450  ustbas2  20463  ustbas  20465  psmetf  20545  psmet0  20547  psmettri2  20548  metflem  20566  xmetf  20567  xmeteq0  20576  xmettri2  20578  tmsxms  20724  tmsms  20725  metustsymOLD  20799  metustsym  20800  tngnrg  20918  cncff  21132  cncfi  21133  cfili  21442  iscmet3lem2  21466  mbfres  21786  mbfimaopnlem  21797  limcresi  22024  dvcnp2  22058  ulmcl  22510  ulmf  22511  ulmcau  22524  pserulm  22551  pserdvlem2  22557  sinq34lt0t  22635  logtayl  22769  dchrmhm  23244  lgsdir2lem2  23327  2sqlem9  23376  mulog2sum  23450  eleei  23876  uhgraf  23975  ushgraf  23978  umgraf2  23993  uslgraf  24021  usgraf  24022  usgraf0  24024  clwwisshclww  24483  frisusgrapr  24667  tncp  24856  grpofo  24877  grpolidinv  24879  grpoass  24881  opidon  25000  isexid2  25003  nvvop  25178  phpar  25415  pjch1  26264  toslub  27318  tosglb  27320  orngsqr  27457  zhmnrg  27584  issgon  27763  measfrge0  27814  measvnul  27817  measvun  27820  fzssfzo  28130  fprodcnv  28690  elpredim  28833  orderseqlem  28909  hfun  29412  hfsn  29413  hfelhf  29415  hfuni  29418  hfpw  29419  fneuni  29748  ptfinfin  29770  heibor1lem  29908  heiborlem1  29910  heiborlem3  29912  lnrfg  30672  elfzop1le2  31055  elprn1  31175  elprn2  31176  stoweidlem35  31335  afvelrnb0  31716  afvelima  31719  rlimdmafv  31729  uhgf  31837  mgmimp  31926  mgmplusgiop  31961  assasslaw  31964  linindsi  32121  trintALTVD  32760  trintALT  32761  bnj916  33070  bnj983  33088  bj-elimhyp  33240  bj-elid  33672  elpcliN  34689  frege55lem1c  36908
  Copyright terms: Public domain W3C validator