Theorem biimpi 186

Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
biimpi.1	|- (ph <-> ps)

Assertion

Ref	Expression
biimpi	|- (ph -> ps)

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimpi.1	. 2 |- (ph <-> ps)
2		bi1 178	. 2 |- ((ph <-> ps) -> (ph -> ps))
3	1, 2	ax-mp 5	1 |- (ph -> ps)

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

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 177

This theorem is referenced by:  sylbi  187  sylib  188  biimpri  197  mpbi  199  syl5bi  208  syl6ib  217  syl7bi  221  syl8ib  222  bitri  240  pm2.53  362  simplbi  446  simprbi  450  sylanb  458  sylan2b  461  pm3.1  484  orbi2i  505  pm2.32  512  anc2l  538  pm3.37  562  dfbi  610  pm2.76  821  pm5.15  859  pm5.16  860  pm5.75  903  rnlem  931  simp1bi  970  simp2bi  971  simp3bi  972  syl3an1b  1218  syl3an2b  1219  syl3an3b  1220  nic-ax  1438  19.25  1603  sbbii  1653  spvw  1666  hbn1fw  1705  excomim  1742  stdpc5  1798  ax10-16  2190  exmoeu  2246  2mo  2282  eqeq1  2359  eleq2  2414  gencbvex  2902  moeq  3013  euind  3024  reuind  3040  eqsbc2  3104  ssel  3268  unssd  3440  ssind  3480  n0moeu  3563  ss0  3582  uneqdifeq  3639  ssunsn2  3866  eqsn  3868  snex  4112  pwadjoin  4120  prprc2  4123  opkelimagekg  4272  iotabi  4349  uniabio  4350  iotaint  4353  dfiota4  4373  nnsucelrlem3  4427  nnsucelr  4429  nndisjeq  4430  preaddccan2  4456  ltfintri  4467  ssfin  4471  eqtfinrelk  4487  tfinsuc  4499  phi011lem1  4599  phidisjnn  4616  dmxp  4924  resabs1  4993  resima2  5008  imasn  5019  funun  5147  funcnv3  5158  funimass1  5170  funssxp  5234  f1ocnv  5300  f1o00  5318  fsn2  5435  fconst5  5456  oprabid  5551  eloprabga  5579  op1st2nd  5791  pw1fnf1o  5856  clos1induct  5881  peano4nc  6151  dflec2  6211  ce2le  6234  addccan2nc  6266  nchoice  6309