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  770  pm2.32  777  oranim  789  stabnot  841  exmiddc  844  pm2.1dc  845  stdcndcOLD  854  stdcn  855  const  860  imanst  896  pm5.75  971  rnlem  985  ifpnst  997  simp1bi  1039  simp2bi  1040  simp3bi  1041  syl3an1b  1310  syl3an2b  1311  syl3an3b  1312  exalim  1551  nford  1616  nfal  1625  stdpc5  1633  sbbii  1814  sb9i  2034  eu5  2128  exmoeudc  2144  eqeq1  2239  eleq2  2296  nner  2416  rexalim  2535  gencbvex  2861  gencbval  2863  moeq  2992  euind  3004  reuind  3022  ssel  3232  ssrmof  3301  unssd  3395  ssind  3445  unssdif  3456  ss0  3549  rabsnif  3758  prprc  3802  disjnim  4099  trint  4223  snexprc  4299  undifexmid  4306  exmidn0m  4314  exmidsssn  4315  exmidundif  4319  exmidundifim  4320  exmid1stab  4321  pocl  4424  sotritrieq  4446  frirrg  4471  unexg  4564  abnex  4568  reusv3i  4580  ordtriexmid  4643  ontriexmidim  4644  ordtri2orexmid  4645  preleq  4677  0elsucexmid  4687  ordpwsucexmid  4692  ordtri2or2exmid  4693  elomssom  4727  brrelex12  4788  0nelrel  4796  elrel  4852  xpssres  5073  elres  5074  coi2  5279  iotabi  5322  uniabio  5323  nfunv  5385  funun  5397  funcnv3  5418  funimass1  5433  imain  5438  funssxp  5532  f0dom0  5561  f1o00  5651  fsn2  5851  funopsn  5860  isoselem  5993  oprabid  6082  brabvv  6099  uchoice  6331  oprssdmm  6365  1stdm  6376  f1o2ndf1  6424  poxp  6428  suppval1  6439  funsssuppss  6458  rdgon  6617  frecfcllem  6635  nntri3or  6726  nntri1  6729  ensym  7021  en2  7065  xpen  7098  snnen2oprc  7114  phplem4on  7122  fict  7123  fidceq  7124  infiexmid  7134  php5fin  7139  fisbth  7140  fin0  7142  fin0or  7143  diffisn  7150  infnfi  7152  fidcen  7156  en2eqpr  7167  exmidpw  7168  exmidpweq  7169  pw1fin  7170  fientri3  7175  unsnfi  7179  unsnfidcex  7180  unsnfidcel  7181  undifdcss  7183  ssfidc  7198  relcnvfi  7208  fiuni  7265  eqinfti  7311  djulclb  7346  updjud  7373  omp1eomlem  7385  0ct  7398  ctmlemr  7399  ctssdclemn0  7401  ctssdccl  7402  enomnilem  7429  finomni  7431  exmidomni  7433  enmkvlem  7452  enwomnilem  7460  exmidontriimlem1  7528  onntri35  7547  onntri52  7554  dftap2  7565  exmidapne  7574  enq0sym  7747  enq0tr  7749  prarloclem3  7812  nqprl  7866  nqpru  7867  addnqprlemrl  7872  addnqprlemru  7873  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemrl  7888  mulnqprlemru  7889  mulnqprlemfl  7890  mulnqprlemfu  7891  ltexprlemfl  7924  ltexprlemfu  7926  recexprlemopl  7940  recexprlemopu  7942  aptipr  7956  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  caucvgprlemladdfu  7992  caucvgprprlemexbt  8021  suplocexprlemrl  8032  suplocexprlemru  8034  suplocexprlemex  8037  srpospr  8098  elrealeu  8144  axarch  8206  axcaucvglemres  8214  nn0ge2m1nn  9560  elnn0z  9590  peano2z  9613  uzm1  9885  qapne  9971  rpregt0  10000  rpnegap  10019  xnn0dcle  10135  xnn0letri  10136  npnflt  10148  nmnfgt  10151  xaddf  10177  xaddval  10178  xltadd1  10209  xsubge0  10214  xleaddadd  10220  elfz1end  10389  1fv  10473  elfzonlteqm1  10555  qtri3or  10600  exbtwnzlemshrink  10608  rebtwn2zlemshrink  10613  ioom  10620  elicore  10626  modfzo0difsn  10757  modsumfzodifsn  10758  addmodlteq  10760  frecfzennn  10788  seq3f1olemstep  10876  ser0  10895  exp3vallem  10902  facp1  11092  faclbnd  11103  bcn1  11120  hashennnuni  11142  hashcl  11144  hashfz1  11146  hashen  11147  fihashdom  11167  hashun  11169  zfz1isolem1  11212  zfz1iso  11213  lencl  11228  sswrd  11233  swrdswrd  11397  swrdccatin2  11421  pfxccat3  11426  pfxccatpfx1  11428  sqrt0  11689  resqrexlemfp1  11694  cau3lem  11799  xrmaxifle  11931  xrmaxiflemval  11935  xrmaxltsup  11943  xrmaxadd  11946  climserle  12030  climcaucn  12036  iserabs  12161  isumshft  12176  cvgratgt0  12219  mertenslem2  12222  prodf1  12228  fprodunsn  12290  fprodfac  12301  eirrap  12464  bezoutlemzz  12698  dfgcd3  12706  nnmindc  12730  nnminle  12731  nninfctlemfo  12736  lcmcllem  12764  prmind2  12817  prm2orodd  12823  sqrt2irr0  12861  sqrt2irrap  12877  ballotfilem2  13142  ennnfonelemjn  13153  ennnfonelemdm  13171  ennnfonelemim  13175  ctiunctlemfo  13190  isstructr  13227  basmex  13272  dfgrp2  13740  dfgrp3mlem  13811  mulgnngsum  13844  grpissubg  13911  ablsubsub23  14042  rrgmex  14406  lssmex  14503  lidlmex  14623  2idlmex  14649  df2idl2  14657  2idlss  14662  isbasis3g  14911  innei  15028  cnpnei  15084  cncnp2m  15096  cnptopresti  15103  cnptoprest2  15105  imasnopn  15164  xmettx  15375  cdivcncfap  15469  expcncf  15474  cnopnap  15476  ivthinclemdisj  15505  dvrecap  15578  dvmptfsum  15590  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  2lgslem1c  15963  2sqlem10  15998  lfgredg2dom  16127  ausgrusgrben  16163  ausgrumgrien  16165  ausgrusgrien  16166  uspgredg2vlem  16215  uspgredg2v  16216  usgredg2vlem2  16218  ushgredgedg  16221  ushgredgedgloop  16223  griedg0ssusgr  16246  vtxedgfi  16284  vtxlpfi  16285  wlk1walkdom  16354  wlk0prc  16367  clwwlknonex2  16434  eupthi  16444  ex-ceil  16494  bj-nnbist  16516  bj-con1st  16523  bj-charfunbi  16581  bj-sucexg  16692  bj-om  16707  bj-inf2vnlem1  16740  trilpolemisumle  16822  cndcap  16844  trimul0or  16845  gfsumval  16862