Theorem ibi 256

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

Step	Hyp	Ref	Expression
1		ibi.1	. . 3 |- ( ph -> ( ph <-> ps ) )
2	1	biimpd 219	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 52	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  ibir  257  elimh  1030  elimhOLD  1033  elab3gf  3356  elimhyp  4146  elimhyp2v  4147  elimhyp3v  4148  elimhyp4v  4149  elpwi  4168  elsni  4194  elpri  4197  eltpi  4229  snssi  4339  prssi  4353  prelpwi  4915  elxpi  5130  releldmb  5360  relelrnb  5361  elpredim  5692  eloni  5733  limuni2  5786  funeu  5913  fneu  5995  fvelima  6248  eloprabi  7232  fo2ndf  7284  tfrlem9  7481  oeeulem  7681  elqsi  7800  qsel  7826  ecopovsym  7849  elpmi  7876  elmapi  7879  pmsspw  7892  brdomi  7966  undom  8048  mapdom1  8125  ominf  8172  unblem2  8213  unfilem1  8224  fiin  8328  brwdomi  8473  canthwdom  8484  brwdom3i  8488  unxpwdom  8494  scott0  8749  acni  8868  pwcdadom  9038  fin1ai  9115  fin2i  9117  fin4i  9120  ssfin3ds  9152  fin23lem17  9160  fin23lem38  9171  fin23lem39  9172  isfin32i  9187  fin34  9212  isfin7-2  9218  fin1a2lem13  9234  fin12  9235  gchi  9446  wuntr  9527  wununi  9528  wunpw  9529  wunpr  9531  wun0  9540  tskpwss  9574  tskpw  9575  tsken  9576  grutr  9615  grupw  9617  grupr  9619  gruurn  9620  ingru  9637  indpi  9729  eliooord  12233  fzrev3i  12407  elfzole1  12478  elfzolt2  12479  fz1fzo0m1  12515  bcp1nk  13104  rere  13862  nn0abscl  14052  climcl  14230  rlimcl  14234  rlimdm  14282  o1res  14291  rlimdmo1  14348  climcau  14401  caucvgb  14410  fprodcnv  14713  cshws0  15808  restsspw  16092  mreiincl  16256  catidex  16335  catcocl  16346  catass  16347  homa1  16687  homahom2  16688  odulat  17145  dlatjmdi  17197  psrel  17203  psref2  17204  pstr2  17205  reldir  17233  dirdm  17234  dirref  17235  dirtr  17236  dirge  17237  mgmcl  17245  submss  17350  subm0cl  17352  submcl  17353  submmnd  17354  subgsubm  17616  symgbasf1o  17803  symginv  17822  psgneu  17926  odmulg  17973  efgsp1  18150  efgsres  18151  frgpnabl  18278  dprdgrp  18404  dprdf  18405  abvfge0  18822  abveq0  18826  abvmul  18829  abvtri  18830  lbsss  19077  lbssp  19079  lbsind  19080  opsrtoslem2  19485  opsrso  19487  domnchr  19880  cssi  20028  linds1  20149  linds2  20150  lindsind  20156  mdetunilem9  20426  uniopn  20702  iunopn  20703  inopn  20704  fiinopn  20706  eltpsg  20747  basis1  20754  basis2  20755  eltg4i  20764  lmff  21105  t1sep2  21173  cmpfii  21212  ptfinfin  21322  kqhmph  21622  fbasne0  21634  0nelfb  21635  fbsspw  21636  fbasssin  21640  ufli  21718  uffixfr  21727  elfm  21751  fclsopni  21819  fclselbas  21820  ustssxp  22008  ustbasel  22010  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ustfilxp  22016  ustbas2  22029  ustbas  22031  psmetf  22111  psmet0  22113  psmettri2  22114  metflem  22133  xmetf  22134  xmeteq0  22143  xmettri2  22145  tmsxms  22291  tmsms  22292  metustsym  22360  tngnrg  22478  cncff  22696  cncfi  22697  cfili  23066  iscmet3lem2  23090  mbfres  23411  mbfimaopnlem  23422  limcresi  23649  dvcnp2  23683  ulmcl  24135  ulmf  24136  ulmcau  24149  pserulm  24176  pserdvlem2  24182  sinq34lt0t  24261  logtayl  24406  dchrmhm  24966  lgsdir2lem2  25051  2sqlem9  25152  mulog2sum  25226  eleei  25777  uhgrf  25957  ushgrf  25958  upgrf  25981  umgrf  25993  uspgrf  26049  usgrf  26050  usgrfs  26052  nbcplgr  26330  clwlkcompim  26676  tncp  27330  eulplig  27337  grpofo  27353  grpolidinv  27355  grpoass  27357  nvvop  27464  phpar  27679  pjch1  28529  toslub  29668  tosglb  29670  orngsqr  29804  zhmnrg  30011  issgon  30186  measfrge0  30266  measvnul  30269  measvun  30272  fzssfzo  30613  bnj916  31003  bnj983  31021  mfsdisj  31447  mtyf2  31448  maxsta  31451  mvtinf  31452  orderseqlem  31749  hfun  32285  hfsn  32286  hfelhf  32288  hfuni  32291  hfpw  32292  fneuni  32342  bj-elid  33085  mptsnunlem  33185  heibor1lem  33608  heiborlem1  33610  heiborlem3  33612  opidonOLD  33651  isexid2  33654  elpcliN  35179  lnrfg  37689  pwinfi2  37867  frege55lem1c  38210  gneispacef  38433  gneispacef2  38434  gneispacern2  38437  gneispace0nelrn  38438  gneispaceel  38441  gneispacess  38443  trintALTVD  39116  trintALT  39117  eliuniin  39279  eliuniin2  39303  disjrnmpt2  39375  fvelimad  39458  stoweidlem35  40252  saluncl  40537  saldifcl  40539  0sal  40540  sge0resplit  40623  omedm  40713  afvelrnb0  41244  afvelima  41247  rlimdmafv  41257  submgmss  41792  submgmcl  41794  submgmmgm  41795  asslawass  41829  linindsi  42236