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  762  pm2.32  769  oranim  781  stabnot  833  exmiddc  836  pm2.1dc  837  stdcndcOLD  846  stdcn  847  const  852  imanst  888  pm5.75  962  rnlem  976  simp1bi  1012  simp2bi  1013  simp3bi  1014  syl3an1b  1274  syl3an2b  1275  syl3an3b  1276  exalim  1502  nford  1567  nfal  1576  stdpc5  1584  sbbii  1765  sb9i  1980  eu5  2073  exmoeudc  2089  eqeq1  2184  eleq2  2241  nner  2351  rexalim  2470  gencbvex  2784  gencbval  2786  moeq  2913  euind  2925  reuind  2943  ssel  3150  ssrmof  3219  unssd  3312  ssind  3360  unssdif  3371  ss0  3464  prprc  3703  disjnim  3995  trint  4117  snexprc  4187  undifexmid  4194  exmidn0m  4202  exmidsssn  4203  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  pocl  4304  sotritrieq  4326  frirrg  4351  unexg  4444  abnex  4448  reusv3i  4460  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  preleq  4555  0elsucexmid  4565  ordpwsucexmid  4570  ordtri2or2exmid  4571  elomssom  4605  brrelex12  4665  0nelrel  4673  elrel  4729  xpssres  4943  elres  4944  coi2  5146  iotabi  5188  uniabio  5189  nfunv  5250  funun  5261  funcnv3  5279  funimass1  5294  imain  5299  funssxp  5386  f0dom0  5410  f1o00  5497  fsn2  5691  isoselem  5821  oprabid  5907  brabvv  5921  oprssdmm  6172  1stdm  6183  f1o2ndf1  6229  poxp  6233  rdgon  6387  frecfcllem  6405  nntri3or  6494  nntri1  6497  ensym  6781  xpen  6845  snnen2oprc  6860  phplem4on  6867  fict  6868  fidceq  6869  infiexmid  6877  php5fin  6882  fisbth  6883  fin0  6885  fin0or  6886  diffisn  6893  infnfi  6895  en2eqpr  6907  exmidpw  6908  exmidpweq  6909  pw1fin  6910  fientri3  6914  unsnfi  6918  unsnfidcex  6919  unsnfidcel  6920  undifdcss  6922  ssfidc  6934  relcnvfi  6940  fiuni  6977  eqinfti  7019  djulclb  7054  updjud  7081  omp1eomlem  7093  0ct  7106  ctmlemr  7107  ctssdclemn0  7109  ctssdccl  7110  enomnilem  7136  finomni  7138  exmidomni  7140  enmkvlem  7159  enwomnilem  7167  exmidontriimlem1  7220  onntri35  7236  onntri52  7243  dftap2  7250  exmidapne  7259  enq0sym  7431  enq0tr  7433  prarloclem3  7496  nqprl  7550  nqpru  7551  addnqprlemrl  7556  addnqprlemru  7557  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemrl  7572  mulnqprlemru  7573  mulnqprlemfl  7574  mulnqprlemfu  7575  ltexprlemfl  7608  ltexprlemfu  7610  recexprlemopl  7624  recexprlemopu  7626  aptipr  7640  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  caucvgprlemladdfu  7676  caucvgprprlemexbt  7705  suplocexprlemrl  7716  suplocexprlemru  7718  suplocexprlemex  7721  srpospr  7782  elrealeu  7828  axarch  7890  axcaucvglemres  7898  nn0ge2m1nn  9236  elnn0z  9266  peano2z  9289  uzm1  9558  qapne  9639  rpregt0  9667  rpnegap  9686  xnn0dcle  9802  xnn0letri  9803  npnflt  9815  nmnfgt  9818  xaddf  9844  xaddval  9845  xltadd1  9876  xsubge0  9881  xleaddadd  9887  elfz1end  10055  1fv  10139  elfzonlteqm1  10210  qtri3or  10243  exbtwnzlemshrink  10249  rebtwn2zlemshrink  10254  ioom  10261  elicore  10267  modfzo0difsn  10395  modsumfzodifsn  10396  addmodlteq  10398  frecfzennn  10426  seq3f1olemstep  10501  ser0  10514  exp3vallem  10521  facp1  10710  faclbnd  10721  bcn1  10738  hashennnuni  10759  hashcl  10761  hashfz1  10763  hashen  10764  fihashdom  10783  hashun  10785  zfz1isolem1  10820  zfz1iso  10821  sqrt0  11013  resqrexlemfp1  11018  cau3lem  11123  xrmaxifle  11254  xrmaxiflemval  11258  xrmaxltsup  11266  xrmaxadd  11269  climserle  11353  climcaucn  11359  iserabs  11483  isumshft  11498  cvgratgt0  11541  mertenslem2  11544  prodf1  11550  fprodunsn  11612  fprodfac  11623  eirrap  11785  bezoutlemzz  12003  dfgcd3  12011  nnmindc  12035  nnminle  12036  lcmcllem  12067  prmind2  12120  prm2orodd  12126  sqrt2irr0  12164  sqrt2irrap  12180  ennnfonelemjn  12403  ennnfonelemdm  12421  ennnfonelemim  12425  ctiunctlemfo  12440  isstructr  12477  basmex  12521  dfgrp2  12902  dfgrp3mlem  12968  grpissubg  13054  ablsubsub23  13128  isbasis3g  13549  innei  13666  cnpnei  13722  cncnp2m  13734  cnptopresti  13741  cnptoprest2  13743  imasnopn  13802  xmettx  14013  cdivcncfap  14090  expcncf  14095  cnopnap  14097  ivthinclemdisj  14121  dvrecap  14180  2sqlem10  14475  ex-ceil  14481  bj-nnbist  14499  bj-con1st  14506  bj-charfunbi  14566  bj-sucexg  14677  bj-om  14692  bj-inf2vnlem1  14725  trilpolemisumle  14789