Theorem biimpi 120

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbi  121  sylib  122  sylbb  123  biimpri  133  mpbi  145  biimtrid  152  imbitrdi  161  syl7bi  165  syl8ib  166  bitri  184  simplbi  274  simprbi  275  sylanb  284  sylan2b  287  anc2l  327  sylanblc  415  orbi2i  767  pm2.32  774  oranim  786  stabnot  838  exmiddc  841  pm2.1dc  842  stdcndcOLD  851  stdcn  852  const  857  imanst  893  pm5.75  968  rnlem  982  ifpnst  994  simp1bi  1036  simp2bi  1037  simp3bi  1038  syl3an1b  1307  syl3an2b  1308  syl3an3b  1309  exalim  1548  nford  1613  nfal  1622  stdpc5  1630  sbbii  1811  sb9i  2031  eu5  2125  exmoeudc  2141  eqeq1  2236  eleq2  2293  nner  2404  rexalim  2523  gencbvex  2847  gencbval  2849  moeq  2978  euind  2990  reuind  3008  ssel  3218  ssrmof  3287  unssd  3380  ssind  3428  unssdif  3439  ss0  3532  prprc  3777  disjnim  4073  trint  4197  snexprc  4270  undifexmid  4277  exmidn0m  4285  exmidsssn  4286  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  pocl  4394  sotritrieq  4416  frirrg  4441  unexg  4534  abnex  4538  reusv3i  4550  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  preleq  4647  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  elomssom  4697  brrelex12  4757  0nelrel  4765  elrel  4821  xpssres  5040  elres  5041  coi2  5245  iotabi  5288  uniabio  5289  nfunv  5351  funun  5362  funcnv3  5383  funimass1  5398  imain  5403  funssxp  5495  f0dom0  5521  f1o00  5610  fsn2  5811  funopsn  5819  isoselem  5950  oprabid  6039  brabvv  6056  uchoice  6289  oprssdmm  6323  1stdm  6334  f1o2ndf1  6380  poxp  6384  rdgon  6538  frecfcllem  6556  nntri3or  6647  nntri1  6650  ensym  6941  en2  6981  xpen  7014  snnen2oprc  7029  phplem4on  7037  fict  7038  fidceq  7039  infiexmid  7047  php5fin  7052  fisbth  7053  fin0  7055  fin0or  7056  diffisn  7063  infnfi  7065  fidcen  7069  en2eqpr  7080  exmidpw  7081  exmidpweq  7082  pw1fin  7083  fientri3  7088  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  undifdcss  7096  ssfidc  7110  relcnvfi  7119  fiuni  7156  eqinfti  7198  djulclb  7233  updjud  7260  omp1eomlem  7272  0ct  7285  ctmlemr  7286  ctssdclemn0  7288  ctssdccl  7289  enomnilem  7316  finomni  7318  exmidomni  7320  enmkvlem  7339  enwomnilem  7347  exmidontriimlem1  7414  onntri35  7433  onntri52  7440  dftap2  7448  exmidapne  7457  enq0sym  7630  enq0tr  7632  prarloclem3  7695  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemrl  7771  mulnqprlemru  7772  mulnqprlemfl  7773  mulnqprlemfu  7774  ltexprlemfl  7807  ltexprlemfu  7809  recexprlemopl  7823  recexprlemopu  7825  aptipr  7839  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemladdfu  7875  caucvgprprlemexbt  7904  suplocexprlemrl  7915  suplocexprlemru  7917  suplocexprlemex  7920  srpospr  7981  elrealeu  8027  axarch  8089  axcaucvglemres  8097  nn0ge2m1nn  9440  elnn0z  9470  peano2z  9493  uzm1  9765  qapne  9846  rpregt0  9875  rpnegap  9894  xnn0dcle  10010  xnn0letri  10011  npnflt  10023  nmnfgt  10026  xaddf  10052  xaddval  10053  xltadd1  10084  xsubge0  10089  xleaddadd  10095  elfz1end  10263  1fv  10347  elfzonlteqm1  10428  qtri3or  10472  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  ioom  10492  elicore  10498  modfzo0difsn  10629  modsumfzodifsn  10630  addmodlteq  10632  frecfzennn  10660  seq3f1olemstep  10748  ser0  10767  exp3vallem  10774  facp1  10964  faclbnd  10975  bcn1  10992  hashennnuni  11013  hashcl  11015  hashfz1  11017  hashen  11018  fihashdom  11037  hashun  11039  zfz1isolem1  11075  zfz1iso  11076  lencl  11088  sswrd  11093  swrdswrd  11252  swrdccatin2  11276  pfxccat3  11281  pfxccatpfx1  11283  sqrt0  11530  resqrexlemfp1  11535  cau3lem  11640  xrmaxifle  11772  xrmaxiflemval  11776  xrmaxltsup  11784  xrmaxadd  11787  climserle  11871  climcaucn  11877  iserabs  12001  isumshft  12016  cvgratgt0  12059  mertenslem2  12062  prodf1  12068  fprodunsn  12130  fprodfac  12141  eirrap  12304  bezoutlemzz  12538  dfgcd3  12546  nnmindc  12570  nnminle  12571  nninfctlemfo  12576  lcmcllem  12604  prmind2  12657  prm2orodd  12663  sqrt2irr0  12701  sqrt2irrap  12717  ennnfonelemjn  12988  ennnfonelemdm  13006  ennnfonelemim  13010  ctiunctlemfo  13025  isstructr  13062  basmex  13107  dfgrp2  13575  dfgrp3mlem  13646  mulgnngsum  13679  grpissubg  13746  ablsubsub23  13877  rrgmex  14240  lssmex  14334  lidlmex  14454  2idlmex  14480  df2idl2  14488  2idlss  14493  isbasis3g  14735  innei  14852  cnpnei  14908  cncnp2m  14920  cnptopresti  14927  cnptoprest2  14929  imasnopn  14988  xmettx  15199  cdivcncfap  15293  expcncf  15298  cnopnap  15300  ivthinclemdisj  15329  dvrecap  15402  dvmptfsum  15414  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  2lgslem1c  15784  2sqlem10  15819  lfgredg2dom  15945  ausgrusgrben  15981  ausgrumgrien  15983  ausgrusgrien  15984  uspgredg2vlem  16033  uspgredg2v  16034  usgredg2vlem2  16036  ushgredgedg  16039  ushgredgedgloop  16041  vtxedgfi  16048  vtxlpfi  16049  wlk1walkdom  16100  wlk0prc  16113  ex-ceil  16145  bj-nnbist  16163  bj-con1st  16170  bj-charfunbi  16229  bj-sucexg  16340  bj-om  16355  bj-inf2vnlem1  16388  trilpolemisumle  16466  cndcap  16487