Theorem biimpi 118

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 116	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
3	1, 2	ax-mp 7	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylbi  119  sylib  120  sylbb  121  biimpri  131  mpbi  143  syl5bi  150  syl6ib  159  syl7bi  163  syl8ib  164  bitri  182  simplbi  268  simprbi  269  sylanb  278  sylan2b  281  anc2l  320  sylanblc  406  orbi2i  711  pm2.32  718  stabnot  774  exmiddc  777  pm2.1dc  778  oranim  840  stabtestimpdc  857  pm5.75  903  rnlem  917  simp1bi  953  simp2bi  954  simp3bi  955  syl3an1b  1205  syl3an2b  1206  syl3an3b  1207  exalim  1431  nford  1499  stdpc5  1516  sbbii  1688  sb9i  1897  eu5  1988  exmoeudc  2004  eqeq1  2087  eleq2  2142  nner  2249  rexalim  2361  gencbvex  2645  gencbval  2647  moeq  2767  euind  2779  reuind  2795  ssel  2993  unssd  3148  ssind  3190  unssdif  3199  ss0  3284  prprc  3502  trint  3890  snexprc  3958  pocl  4058  sotritrieq  4080  frirrg  4105  unexg  4196  reusv3i  4209  ordtriexmid  4265  ordtri2orexmid  4266  preleq  4298  0elsucexmid  4308  ordpwsucexmid  4313  ordtri2or2exmid  4314  elnn  4346  brrelex12  4399  elrel  4460  xpssres  4663  elres  4664  coi2  4857  iotabi  4896  uniabio  4897  nfunv  4953  funun  4964  funcnv3  4981  funimass1  4996  imain  5001  funssxp  5080  f1o00  5181  fsn2  5358  isoselem  5479  oprabid  5557  brabvv  5571  1stdm  5828  f1o2ndf1  5869  poxp  5873  nntri3or  6095  nntri1  6097  ensym  6284  snnen2oprc  6346  phplem4on  6353  fidceq  6354  infiexmid  6362  php5fin  6366  fisbth  6367  fin0  6369  fin0or  6370  diffisn  6377  en2eqpr  6380  fientri3  6381  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  relcnvfi  6391  eqinfti  6433  enq0sym  6622  enq0tr  6624  prarloclem3  6687  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemrl  6763  mulnqprlemru  6764  mulnqprlemfl  6765  mulnqprlemfu  6766  ltexprlemfl  6799  ltexprlemfu  6801  recexprlemopl  6815  recexprlemopu  6817  aptipr  6831  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  caucvgprlemladdfu  6867  caucvgprprlemexbt  6896  srpospr  6959  elrealeu  6998  axarch  7057  axcaucvglemres  7065  nn0ge2m1nn  8348  elnn0z  8364  peano2z  8387  uzm1  8649  qapne  8724  rpregt0  8747  rpnegap  8766  elfz1end  9074  1fv  9149  elfzonlteqm1  9219  qtri3or  9252  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  ioom  9269  modfzo0difsn  9397  modsumfzodifsn  9398  addmodlteq  9400  frecfzennn  9419  iser0  9471  expival  9478  facp1  9657  faclbnd  9668  bcn1  9685  sqrt0  9890  resqrexlemfp1  9895  cau3lem  10000  climcaucn  10188  bezoutlemzz  10391  dfgcd3  10399  lcmcllem  10449  prmind2  10502  prm2orodd  10508  sqrt2irrap  10558  ex-ceil  10564  bj-sucexg  10713  bj-om  10732  bj-inf2vnlem1  10765