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  2848  gencbval  2850  moeq  2979  euind  2991  reuind  3009  ssel  3219  ssrmof  3288  unssd  3381  ssind  3429  unssdif  3440  ss0  3533  rabsnif  3736  prprc  3780  disjnim  4076  trint  4200  snexprc  4274  undifexmid  4281  exmidn0m  4289  exmidsssn  4290  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  pocl  4398  sotritrieq  4420  frirrg  4445  unexg  4538  abnex  4542  reusv3i  4554  ordtriexmid  4617  ontriexmidim  4618  ordtri2orexmid  4619  preleq  4651  0elsucexmid  4661  ordpwsucexmid  4666  ordtri2or2exmid  4667  elomssom  4701  brrelex12  4762  0nelrel  4770  elrel  4826  xpssres  5046  elres  5047  coi2  5251  iotabi  5294  uniabio  5295  nfunv  5357  funun  5368  funcnv3  5389  funimass1  5404  imain  5409  funssxp  5501  f0dom0  5527  f1o00  5616  fsn2  5817  funopsn  5825  isoselem  5956  oprabid  6045  brabvv  6062  uchoice  6295  oprssdmm  6329  1stdm  6340  f1o2ndf1  6388  poxp  6392  rdgon  6547  frecfcllem  6565  nntri3or  6656  nntri1  6659  ensym  6950  en2  6993  xpen  7026  snnen2oprc  7041  phplem4on  7049  fict  7050  fidceq  7051  infiexmid  7059  php5fin  7064  fisbth  7065  fin0  7067  fin0or  7068  diffisn  7075  infnfi  7077  fidcen  7081  en2eqpr  7092  exmidpw  7093  exmidpweq  7094  pw1fin  7095  fientri3  7100  unsnfi  7104  unsnfidcex  7105  unsnfidcel  7106  undifdcss  7108  ssfidc  7122  relcnvfi  7131  fiuni  7168  eqinfti  7210  djulclb  7245  updjud  7272  omp1eomlem  7284  0ct  7297  ctmlemr  7298  ctssdclemn0  7300  ctssdccl  7301  enomnilem  7328  finomni  7330  exmidomni  7332  enmkvlem  7351  enwomnilem  7359  exmidontriimlem1  7426  onntri35  7445  onntri52  7452  dftap2  7460  exmidapne  7469  enq0sym  7642  enq0tr  7644  prarloclem3  7707  nqprl  7761  nqpru  7762  addnqprlemrl  7767  addnqprlemru  7768  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemrl  7783  mulnqprlemru  7784  mulnqprlemfl  7785  mulnqprlemfu  7786  ltexprlemfl  7819  ltexprlemfu  7821  recexprlemopl  7835  recexprlemopu  7837  aptipr  7851  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  caucvgprlemladdfu  7887  caucvgprprlemexbt  7916  suplocexprlemrl  7927  suplocexprlemru  7929  suplocexprlemex  7932  srpospr  7993  elrealeu  8039  axarch  8101  axcaucvglemres  8109  nn0ge2m1nn  9452  elnn0z  9482  peano2z  9505  uzm1  9777  qapne  9863  rpregt0  9892  rpnegap  9911  xnn0dcle  10027  xnn0letri  10028  npnflt  10040  nmnfgt  10043  xaddf  10069  xaddval  10070  xltadd1  10101  xsubge0  10106  xleaddadd  10112  elfz1end  10280  1fv  10364  elfzonlteqm1  10445  qtri3or  10490  exbtwnzlemshrink  10498  rebtwn2zlemshrink  10503  ioom  10510  elicore  10516  modfzo0difsn  10647  modsumfzodifsn  10648  addmodlteq  10650  frecfzennn  10678  seq3f1olemstep  10766  ser0  10785  exp3vallem  10792  facp1  10982  faclbnd  10993  bcn1  11010  hashennnuni  11031  hashcl  11033  hashfz1  11035  hashen  11036  fihashdom  11056  hashun  11058  zfz1isolem1  11094  zfz1iso  11095  lencl  11107  sswrd  11112  swrdswrd  11276  swrdccatin2  11300  pfxccat3  11305  pfxccatpfx1  11307  sqrt0  11555  resqrexlemfp1  11560  cau3lem  11665  xrmaxifle  11797  xrmaxiflemval  11801  xrmaxltsup  11809  xrmaxadd  11812  climserle  11896  climcaucn  11902  iserabs  12026  isumshft  12041  cvgratgt0  12084  mertenslem2  12087  prodf1  12093  fprodunsn  12155  fprodfac  12166  eirrap  12329  bezoutlemzz  12563  dfgcd3  12571  nnmindc  12595  nnminle  12596  nninfctlemfo  12601  lcmcllem  12629  prmind2  12682  prm2orodd  12688  sqrt2irr0  12726  sqrt2irrap  12742  ennnfonelemjn  13013  ennnfonelemdm  13031  ennnfonelemim  13035  ctiunctlemfo  13050  isstructr  13087  basmex  13132  dfgrp2  13600  dfgrp3mlem  13671  mulgnngsum  13704  grpissubg  13771  ablsubsub23  13902  rrgmex  14265  lssmex  14359  lidlmex  14479  2idlmex  14505  df2idl2  14513  2idlss  14518  isbasis3g  14760  innei  14877  cnpnei  14933  cncnp2m  14945  cnptopresti  14952  cnptoprest2  14954  imasnopn  15013  xmettx  15224  cdivcncfap  15318  expcncf  15323  cnopnap  15325  ivthinclemdisj  15354  dvrecap  15427  dvmptfsum  15439  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  2lgslem1c  15809  2sqlem10  15844  lfgredg2dom  15971  ausgrusgrben  16007  ausgrumgrien  16009  ausgrusgrien  16010  uspgredg2vlem  16059  uspgredg2v  16060  usgredg2vlem2  16062  ushgredgedg  16065  ushgredgedgloop  16067  griedg0ssusgr  16090  vtxedgfi  16095  vtxlpfi  16096  wlk1walkdom  16156  wlk0prc  16169  clwwlknonex2  16234  eupthi  16244  ex-ceil  16258  bj-nnbist  16276  bj-con1st  16283  bj-charfunbi  16342  bj-sucexg  16453  bj-om  16468  bj-inf2vnlem1  16501  trilpolemisumle  16578  cndcap  16599