Theorem biimpi 119

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbi  120  sylib  121  sylbb  122  biimpri  132  mpbi  144  syl5bi  151  syl6ib  160  syl7bi  164  syl8ib  165  bitri  183  simplbi  272  simprbi  273  sylanb  282  sylan2b  285  anc2l  325  sylanblc  413  orbi2i  757  pm2.32  764  oranim  776  stabnot  828  exmiddc  831  pm2.1dc  832  stdcndcOLD  841  stdcn  842  const  847  imanst  883  pm5.75  957  rnlem  971  simp1bi  1007  simp2bi  1008  simp3bi  1009  syl3an1b  1269  syl3an2b  1270  syl3an3b  1271  exalim  1495  nford  1560  nfal  1569  stdpc5  1577  sbbii  1758  sb9i  1973  eu5  2066  exmoeudc  2082  eqeq1  2177  eleq2  2234  nner  2344  rexalim  2463  gencbvex  2776  gencbval  2778  moeq  2905  euind  2917  reuind  2935  ssel  3141  ssrmof  3210  unssd  3303  ssind  3351  unssdif  3362  ss0  3454  prprc  3691  disjnim  3978  trint  4100  snexprc  4170  undifexmid  4177  exmidn0m  4185  exmidsssn  4186  exmidundif  4190  exmidundifim  4191  pocl  4286  sotritrieq  4308  frirrg  4333  unexg  4426  abnex  4430  reusv3i  4442  ordtriexmid  4503  ontriexmidim  4504  ordtri2orexmid  4505  preleq  4537  0elsucexmid  4547  ordpwsucexmid  4552  ordtri2or2exmid  4553  elomssom  4587  brrelex12  4647  0nelrel  4655  elrel  4711  xpssres  4924  elres  4925  coi2  5125  iotabi  5167  uniabio  5168  nfunv  5229  funun  5240  funcnv3  5258  funimass1  5273  imain  5278  funssxp  5365  f0dom0  5389  f1o00  5475  fsn2  5667  isoselem  5796  oprabid  5882  brabvv  5896  oprssdmm  6147  1stdm  6158  f1o2ndf1  6204  poxp  6208  rdgon  6362  frecfcllem  6380  nntri3or  6469  nntri1  6472  ensym  6755  xpen  6819  snnen2oprc  6834  phplem4on  6841  fict  6842  fidceq  6843  infiexmid  6851  php5fin  6856  fisbth  6857  fin0  6859  fin0or  6860  diffisn  6867  infnfi  6869  en2eqpr  6881  exmidpw  6882  exmidpweq  6883  pw1fin  6884  fientri3  6888  unsnfi  6892  unsnfidcex  6893  unsnfidcel  6894  undifdcss  6896  ssfidc  6908  relcnvfi  6914  fiuni  6951  eqinfti  6993  djulclb  7028  updjud  7055  omp1eomlem  7067  0ct  7080  ctmlemr  7081  ctssdclemn0  7083  ctssdccl  7084  enomnilem  7110  finomni  7112  exmidomni  7114  enmkvlem  7133  enwomnilem  7141  exmidontriimlem1  7185  onntri35  7201  onntri52  7208  enq0sym  7381  enq0tr  7383  prarloclem3  7446  nqprl  7500  nqpru  7501  addnqprlemrl  7506  addnqprlemru  7507  addnqprlemfl  7508  addnqprlemfu  7509  mulnqprlemrl  7522  mulnqprlemru  7523  mulnqprlemfl  7524  mulnqprlemfu  7525  ltexprlemfl  7558  ltexprlemfu  7560  recexprlemopl  7574  recexprlemopu  7576  aptipr  7590  cauappcvgprlemladdfu  7603  cauappcvgprlemladdfl  7604  caucvgprlemladdfu  7626  caucvgprprlemexbt  7655  suplocexprlemrl  7666  suplocexprlemru  7668  suplocexprlemex  7671  srpospr  7732  elrealeu  7778  axarch  7840  axcaucvglemres  7848  nn0ge2m1nn  9182  elnn0z  9212  peano2z  9235  uzm1  9504  qapne  9585  rpregt0  9611  rpnegap  9630  xnn0dcle  9746  xnn0letri  9747  npnflt  9759  nmnfgt  9762  xaddf  9788  xaddval  9789  xltadd1  9820  xsubge0  9825  xleaddadd  9831  elfz1end  9998  1fv  10082  elfzonlteqm1  10153  qtri3or  10186  exbtwnzlemshrink  10192  rebtwn2zlemshrink  10197  ioom  10204  elicore  10210  modfzo0difsn  10338  modsumfzodifsn  10339  addmodlteq  10341  frecfzennn  10369  seq3f1olemstep  10444  ser0  10457  exp3vallem  10464  facp1  10651  faclbnd  10662  bcn1  10679  hashennnuni  10700  hashcl  10702  hashfz1  10704  hashen  10705  fihashdom  10725  hashun  10727  zfz1isolem1  10762  zfz1iso  10763  sqrt0  10955  resqrexlemfp1  10960  cau3lem  11065  xrmaxifle  11196  xrmaxiflemval  11200  xrmaxltsup  11208  xrmaxadd  11211  climserle  11295  climcaucn  11301  iserabs  11425  isumshft  11440  cvgratgt0  11483  mertenslem2  11486  prodf1  11492  fprodunsn  11554  fprodfac  11565  eirrap  11727  bezoutlemzz  11944  dfgcd3  11952  nnmindc  11976  nnminle  11977  lcmcllem  12008  prmind2  12061  prm2orodd  12067  sqrt2irr0  12105  sqrt2irrap  12121  ennnfonelemjn  12344  ennnfonelemdm  12362  ennnfonelemim  12366  ctiunctlemfo  12381  isstructr  12418  basmex  12461  dfgrp2  12719  isbasis3g  12797  innei  12916  cnpnei  12972  cncnp2m  12984  cnptopresti  12991  cnptoprest2  12993  imasnopn  13052  xmettx  13263  cdivcncfap  13340  expcncf  13345  cnopnap  13347  ivthinclemdisj  13371  dvrecap  13430  2sqlem10  13714  ex-ceil  13720  bj-nnbist  13738  bj-con1st  13745  bj-charfunbi  13806  bj-sucexg  13917  bj-om  13932  bj-inf2vnlem1  13965  exmid1stab  13993  trilpolemisumle  14030