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  3248  elimhyp  3987  elimhyp2v  3988  elimhyp3v  3989  elimhyp4v  3990  elpwi  4008  elpr2  4035  elpri  4036  elsni  4041  eltpi  4060  snssi  4160  prssi  4172  eloni  4877  limuni2  4928  elxpi  5004  releldmb  5226  relelrnb  5227  funeu  5594  fneu  5667  fvelima  5900  eloprabi  6835  fo2ndf  6880  tfrlem9  7046  oeeulem  7242  elqsi  7357  qsel  7382  ecopovsym  7405  elpmi  7430  elmapi  7433  pmsspw  7446  brdomi  7520  undom  7598  mapdom1  7675  ominf  7725  unblem2  7765  unfilem1  7776  fiin  7874  brwdomi  7986  canthwdom  7997  brwdom3i  8001  unxpwdom  8007  scott0  8295  acni  8417  pwcdadom  8587  fin1ai  8664  fin2i  8666  fin4i  8669  ssfin3ds  8701  fin23lem17  8709  fin23lem38  8720  fin23lem39  8721  isfin32i  8736  fin34  8761  isfin7-2  8767  fin1a2lem13  8783  fin12  8784  gchi  8991  wuntr  9072  wununi  9073  wunpw  9074  wunpr  9076  wun0  9085  tskpwss  9119  tskpw  9120  tsken  9121  grutr  9160  grupw  9162  grupr  9164  gruurn  9165  ingru  9182  indpi  9274  eliooord  11587  fzrev3i  11750  elfzole1  11812  elfzolt2  11813  bcp1nk  12380  rere  13040  nn0abscl  13230  climcl  13407  rlimcl  13411  rlimdm  13459  o1res  13468  rlimdmo1  13525  climcau  13578  caucvgb  13587  fprodcnv  13872  cshws0  14673  restsspw  14924  mreiincl  15088  catidex  15166  catcocl  15177  catass  15178  homa1  15518  homahom2  15519  odulat  15977  dlatjmdi  16029  psrel  16035  psref2  16036  pstr2  16037  reldir  16065  dirdm  16066  dirref  16067  dirtr  16068  dirge  16069  mgmcl  16077  submss  16183  subm0cl  16185  submcl  16186  submmnd  16187  subgsubm  16425  symgbasf1o  16610  symginv  16629  psgneu  16733  odmulg  16780  efgsp1  16957  efgsres  16958  frgpnabl  17081  dprdgrp  17236  dprdf  17237  abvfge0  17669  abveq0  17673  abvmul  17676  abvtri  17677  lbsss  17921  lbssp  17923  lbsind  17924  opsrtoslem2  18347  opsrso  18349  domnchr  18747  cssi  18891  linds1  19015  linds2  19016  lindsind  19022  mdetunilem9  19292  uniopn  19576  iunopn  19577  inopn  19578  fiinopn  19580  eltpsg  19616  basis1  19621  basis2  19622  eltg4i  19631  lmff  19972  t1sep2  20040  cmpfii  20079  ptfinfin  20189  kqhmph  20489  fbasne0  20500  0nelfb  20501  fbsspw  20502  fbasssin  20506  ufli  20584  uffixfr  20593  elfm  20617  fclsopni  20685  fclselbas  20686  ustssxp  20876  ustbasel  20878  ustincl  20879  ustdiag  20880  ustinvel  20881  ustexhalf  20882  ustfilxp  20884  ustbas2  20897  ustbas  20899  psmetf  20979  psmet0  20981  psmettri2  20982  metflem  21000  xmetf  21001  xmeteq0  21010  xmettri2  21012  tmsxms  21158  tmsms  21159  metustsymOLD  21233  metustsym  21234  tngnrg  21352  cncff  21566  cncfi  21567  cfili  21876  iscmet3lem2  21900  mbfres  22220  mbfimaopnlem  22231  limcresi  22458  dvcnp2  22492  ulmcl  22945  ulmf  22946  ulmcau  22959  pserulm  22986  pserdvlem2  22992  sinq34lt0t  23071  logtayl  23212  dchrmhm  23717  lgsdir2lem2  23800  2sqlem9  23849  mulog2sum  23923  eleei  24405  uhgraf  24504  ushgraf  24507  umgraf2  24522  uslgraf  24550  usgraf  24551  usgraf0  24553  clwwisshclww  25012  frisusgrapr  25196  tncp  25385  grpofo  25402  grpolidinv  25404  grpoass  25406  opidonOLD  25525  isexid2  25528  nvvop  25703  phpar  25940  pjch1  26789  toslub  27893  tosglb  27895  orngsqr  28032  zhmnrg  28185  issgon  28356  measfrge0  28414  measvnul  28417  measvun  28420  fzssfzo  28757  mfsdisj  29177  mtyf2  29178  maxsta  29181  mvtinf  29182  elpredim  29499  orderseqlem  29575  hfun  30066  hfsn  30067  hfelhf  30069  hfuni  30072  hfpw  30073  fneuni  30408  heibor1lem  30548  heiborlem1  30550  heiborlem3  30552  lnrfg  31312  stoweidlem35  32059  afvelrnb0  32491  afvelima  32494  rlimdmafv  32504  uhgf  32759  submgmss  32871  submgmcl  32873  submgmmgm  32874  asslawass  32908  linindsi  33321  trintALTVD  34100  trintALT  34101  bnj916  34411  bnj983  34429  bj-elimhyp  34580  bj-elid  35019  elpcliN  36033  pwinfi2  38179  frege55lem1c  38417
  Copyright terms: Public domain W3C validator