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  3776  disjnim  4072  trint  4196  snexprc  4269  undifexmid  4276  exmidn0m  4284  exmidsssn  4285  exmidundif  4289  exmidundifim  4290  exmid1stab  4291  pocl  4393  sotritrieq  4415  frirrg  4440  unexg  4533  abnex  4537  reusv3i  4549  ordtriexmid  4612  ontriexmidim  4613  ordtri2orexmid  4614  preleq  4646  0elsucexmid  4656  ordpwsucexmid  4661  ordtri2or2exmid  4662  elomssom  4696  brrelex12  4756  0nelrel  4764  elrel  4820  xpssres  5039  elres  5040  coi2  5244  iotabi  5287  uniabio  5288  nfunv  5350  funun  5361  funcnv3  5382  funimass1  5397  imain  5402  funssxp  5492  f0dom0  5518  f1o00  5607  fsn2  5808  funopsn  5816  isoselem  5943  oprabid  6032  brabvv  6049  uchoice  6281  oprssdmm  6315  1stdm  6326  f1o2ndf1  6372  poxp  6376  rdgon  6530  frecfcllem  6548  nntri3or  6637  nntri1  6640  ensym  6931  en2  6971  xpen  7002  snnen2oprc  7017  phplem4on  7025  fict  7026  fidceq  7027  infiexmid  7035  php5fin  7040  fisbth  7041  fin0  7043  fin0or  7044  diffisn  7051  infnfi  7053  en2eqpr  7065  exmidpw  7066  exmidpweq  7067  pw1fin  7068  fientri3  7073  unsnfi  7077  unsnfidcex  7078  unsnfidcel  7079  undifdcss  7081  ssfidc  7095  relcnvfi  7104  fiuni  7141  eqinfti  7183  djulclb  7218  updjud  7245  omp1eomlem  7257  0ct  7270  ctmlemr  7271  ctssdclemn0  7273  ctssdccl  7274  enomnilem  7301  finomni  7303  exmidomni  7305  enmkvlem  7324  enwomnilem  7332  exmidontriimlem1  7399  onntri35  7418  onntri52  7425  dftap2  7433  exmidapne  7442  enq0sym  7615  enq0tr  7617  prarloclem3  7680  nqprl  7734  nqpru  7735  addnqprlemrl  7740  addnqprlemru  7741  addnqprlemfl  7742  addnqprlemfu  7743  mulnqprlemrl  7756  mulnqprlemru  7757  mulnqprlemfl  7758  mulnqprlemfu  7759  ltexprlemfl  7792  ltexprlemfu  7794  recexprlemopl  7808  recexprlemopu  7810  aptipr  7824  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  caucvgprlemladdfu  7860  caucvgprprlemexbt  7889  suplocexprlemrl  7900  suplocexprlemru  7902  suplocexprlemex  7905  srpospr  7966  elrealeu  8012  axarch  8074  axcaucvglemres  8082  nn0ge2m1nn  9425  elnn0z  9455  peano2z  9478  uzm1  9749  qapne  9830  rpregt0  9859  rpnegap  9878  xnn0dcle  9994  xnn0letri  9995  npnflt  10007  nmnfgt  10010  xaddf  10036  xaddval  10037  xltadd1  10068  xsubge0  10073  xleaddadd  10079  elfz1end  10247  1fv  10331  elfzonlteqm1  10411  qtri3or  10455  exbtwnzlemshrink  10463  rebtwn2zlemshrink  10468  ioom  10475  elicore  10481  modfzo0difsn  10612  modsumfzodifsn  10613  addmodlteq  10615  frecfzennn  10643  seq3f1olemstep  10731  ser0  10750  exp3vallem  10757  facp1  10947  faclbnd  10958  bcn1  10975  hashennnuni  10996  hashcl  10998  hashfz1  11000  hashen  11001  fihashdom  11020  hashun  11022  zfz1isolem1  11057  zfz1iso  11058  lencl  11070  sswrd  11075  swrdswrd  11232  swrdccatin2  11256  pfxccat3  11261  pfxccatpfx1  11263  sqrt0  11510  resqrexlemfp1  11515  cau3lem  11620  xrmaxifle  11752  xrmaxiflemval  11756  xrmaxltsup  11764  xrmaxadd  11767  climserle  11851  climcaucn  11857  iserabs  11981  isumshft  11996  cvgratgt0  12039  mertenslem2  12042  prodf1  12048  fprodunsn  12110  fprodfac  12121  eirrap  12284  bezoutlemzz  12518  dfgcd3  12526  nnmindc  12550  nnminle  12551  nninfctlemfo  12556  lcmcllem  12584  prmind2  12637  prm2orodd  12643  sqrt2irr0  12681  sqrt2irrap  12697  ennnfonelemjn  12968  ennnfonelemdm  12986  ennnfonelemim  12990  ctiunctlemfo  13005  isstructr  13042  basmex  13087  dfgrp2  13555  dfgrp3mlem  13626  mulgnngsum  13659  grpissubg  13726  ablsubsub23  13857  rrgmex  14219  lssmex  14313  lidlmex  14433  2idlmex  14459  df2idl2  14467  2idlss  14472  isbasis3g  14714  innei  14831  cnpnei  14887  cncnp2m  14899  cnptopresti  14906  cnptoprest2  14908  imasnopn  14967  xmettx  15178  cdivcncfap  15272  expcncf  15277  cnopnap  15279  ivthinclemdisj  15308  dvrecap  15381  dvmptfsum  15393  gausslemma2dlem0i  15730  gausslemma2dlem1a  15731  2lgslem1c  15763  2sqlem10  15798  lfgredg2dom  15924  ausgrusgrben  15960  ausgrumgrien  15962  ausgrusgrien  15963  uspgredg2vlem  16012  uspgredg2v  16013  usgredg2vlem2  16015  ushgredgedg  16018  ushgredgedgloop  16020  ex-ceil  16048  bj-nnbist  16066  bj-con1st  16073  bj-charfunbi  16132  bj-sucexg  16243  bj-om  16258  bj-inf2vnlem1  16291  trilpolemisumle  16365  cndcap  16386