Theorem biimpi 186

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

Hypothesis

Ref	Expression
biimpi.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
biimpi	⊢ (φ → ψ)

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimpi.1	. 2 ⊢ (φ ↔ ψ)
2		bi1 178	. 2 ⊢ ((φ ↔ ψ) → (φ → ψ))
3	1, 2	ax-mp 5	1 ⊢ (φ → ψ)

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  2901  moeq  3012  euind  3023  reuind  3039  eqsbc3r  3103  ssel  3267  unssd  3439  ssind  3479  n0moeu  3562  ss0  3581  uneqdifeq  3638  ssunsn2  3865  eqsn  3867  snex  4111  pwadjoin  4119  prprc2  4122  opkelimagekg  4271  iotabi  4348  uniabio  4349  iotaint  4352  dfiota4  4372  nnsucelrlem3  4426  nnsucelr  4428  nndisjeq  4429  preaddccan2  4455  ltfintri  4466  ssfin  4470  eqtfinrelk  4486  tfinsuc  4498  phi011lem1  4598  phidisjnn  4615  dmxp  4923  resabs1  4992  resima2  5007  imasn  5018  funun  5146  funcnv3  5157  funimass1  5169  funssxp  5233  f1ocnv  5299  f1o00  5317  fsn2  5434  fconst5  5455  oprabid  5550  eloprabga  5578  op1st2nd  5790  pw1fnf1o  5855  clos1induct  5880  peano4nc  6150  dflec2  6210  ce2le  6233  addccan2nc  6265  nchoice  6308