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  764  pm2.32  771  oranim  783  stabnot  835  exmiddc  838  pm2.1dc  839  stdcndcOLD  848  stdcn  849  const  854  imanst  890  pm5.75  965  rnlem  979  simp1bi  1015  simp2bi  1016  simp3bi  1017  syl3an1b  1286  syl3an2b  1287  syl3an3b  1288  exalim  1525  nford  1590  nfal  1599  stdpc5  1607  sbbii  1788  sb9i  2008  eu5  2101  exmoeudc  2117  eqeq1  2212  eleq2  2269  nner  2380  rexalim  2499  gencbvex  2819  gencbval  2821  moeq  2948  euind  2960  reuind  2978  ssel  3187  ssrmof  3256  unssd  3349  ssind  3397  unssdif  3408  ss0  3501  prprc  3743  disjnim  4035  trint  4157  snexprc  4230  undifexmid  4237  exmidn0m  4245  exmidsssn  4246  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  pocl  4350  sotritrieq  4372  frirrg  4397  unexg  4490  abnex  4494  reusv3i  4506  ordtriexmid  4569  ontriexmidim  4570  ordtri2orexmid  4571  preleq  4603  0elsucexmid  4613  ordpwsucexmid  4618  ordtri2or2exmid  4619  elomssom  4653  brrelex12  4713  0nelrel  4721  elrel  4777  xpssres  4994  elres  4995  coi2  5199  iotabi  5241  uniabio  5242  nfunv  5304  funun  5315  funcnv3  5336  funimass1  5351  imain  5356  funssxp  5445  f0dom0  5469  f1o00  5557  fsn2  5754  funopsn  5762  isoselem  5889  oprabid  5976  brabvv  5991  uchoice  6223  oprssdmm  6257  1stdm  6268  f1o2ndf1  6314  poxp  6318  rdgon  6472  frecfcllem  6490  nntri3or  6579  nntri1  6582  ensym  6873  en2  6912  xpen  6942  snnen2oprc  6957  phplem4on  6964  fict  6965  fidceq  6966  infiexmid  6974  php5fin  6979  fisbth  6980  fin0  6982  fin0or  6983  diffisn  6990  infnfi  6992  en2eqpr  7004  exmidpw  7005  exmidpweq  7006  pw1fin  7007  fientri3  7012  unsnfi  7016  unsnfidcex  7017  unsnfidcel  7018  undifdcss  7020  ssfidc  7034  relcnvfi  7043  fiuni  7080  eqinfti  7122  djulclb  7157  updjud  7184  omp1eomlem  7196  0ct  7209  ctmlemr  7210  ctssdclemn0  7212  ctssdccl  7213  enomnilem  7240  finomni  7242  exmidomni  7244  enmkvlem  7263  enwomnilem  7271  exmidontriimlem1  7333  onntri35  7349  onntri52  7356  dftap2  7363  exmidapne  7372  enq0sym  7545  enq0tr  7547  prarloclem3  7610  nqprl  7664  nqpru  7665  addnqprlemrl  7670  addnqprlemru  7671  addnqprlemfl  7672  addnqprlemfu  7673  mulnqprlemrl  7686  mulnqprlemru  7687  mulnqprlemfl  7688  mulnqprlemfu  7689  ltexprlemfl  7722  ltexprlemfu  7724  recexprlemopl  7738  recexprlemopu  7740  aptipr  7754  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemladdfu  7790  caucvgprprlemexbt  7819  suplocexprlemrl  7830  suplocexprlemru  7832  suplocexprlemex  7835  srpospr  7896  elrealeu  7942  axarch  8004  axcaucvglemres  8012  nn0ge2m1nn  9355  elnn0z  9385  peano2z  9408  uzm1  9679  qapne  9760  rpregt0  9789  rpnegap  9808  xnn0dcle  9924  xnn0letri  9925  npnflt  9937  nmnfgt  9940  xaddf  9966  xaddval  9967  xltadd1  9998  xsubge0  10003  xleaddadd  10009  elfz1end  10177  1fv  10261  elfzonlteqm1  10339  qtri3or  10383  exbtwnzlemshrink  10391  rebtwn2zlemshrink  10396  ioom  10403  elicore  10409  modfzo0difsn  10540  modsumfzodifsn  10541  addmodlteq  10543  frecfzennn  10571  seq3f1olemstep  10659  ser0  10678  exp3vallem  10685  facp1  10875  faclbnd  10886  bcn1  10903  hashennnuni  10924  hashcl  10926  hashfz1  10928  hashen  10929  fihashdom  10948  hashun  10950  zfz1isolem1  10985  zfz1iso  10986  lencl  10998  sswrd  11003  sqrt0  11315  resqrexlemfp1  11320  cau3lem  11425  xrmaxifle  11557  xrmaxiflemval  11561  xrmaxltsup  11569  xrmaxadd  11572  climserle  11656  climcaucn  11662  iserabs  11786  isumshft  11801  cvgratgt0  11844  mertenslem2  11847  prodf1  11853  fprodunsn  11915  fprodfac  11926  eirrap  12089  bezoutlemzz  12323  dfgcd3  12331  nnmindc  12355  nnminle  12356  nninfctlemfo  12361  lcmcllem  12389  prmind2  12442  prm2orodd  12448  sqrt2irr0  12486  sqrt2irrap  12502  ennnfonelemjn  12773  ennnfonelemdm  12791  ennnfonelemim  12795  ctiunctlemfo  12810  isstructr  12847  basmex  12891  dfgrp2  13359  dfgrp3mlem  13430  mulgnngsum  13463  grpissubg  13530  ablsubsub23  13661  rrgmex  14023  lssmex  14117  lidlmex  14237  2idlmex  14263  df2idl2  14271  2idlss  14276  isbasis3g  14518  innei  14635  cnpnei  14691  cncnp2m  14703  cnptopresti  14710  cnptoprest2  14712  imasnopn  14771  xmettx  14982  cdivcncfap  15076  expcncf  15081  cnopnap  15083  ivthinclemdisj  15112  dvrecap  15185  dvmptfsum  15197  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  2lgslem1c  15567  2sqlem10  15602  ex-ceil  15662  bj-nnbist  15680  bj-con1st  15687  bj-charfunbi  15747  bj-sucexg  15858  bj-om  15873  bj-inf2vnlem1  15906  trilpolemisumle  15977  cndcap  15998