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  birani  386  bilani  387  sylanblc  419  orbi2i  774  pm2.32  781  oranim  793  stabnot  845  exmiddc  848  pm2.1dc  849  stdcndcOLD  858  stdcn  859  const  864  imanst  900  pm5.75  975  rnlem  989  ifpnst  1001  simp1bi  1043  simp2bi  1044  simp3bi  1045  syl3an1b  1314  syl3an2b  1315  syl3an3b  1316  exalim  1555  nford  1620  nfal  1629  stdpc5  1637  sbbii  1818  sb9i  2040  eu5  2134  exmoeudc  2150  eqeq1  2245  eleq2  2302  nner  2424  rexalim  2543  gencbvex  2869  gencbval  2871  moeq  3001  euind  3013  reuind  3031  ssel  3242  ssrmof  3311  unssd  3405  ssind  3455  unssdif  3466  ss0  3563  rabsnif  3774  prprc  3818  disjnim  4115  trint  4239  snexprc  4318  undifexmid  4325  exmidn0m  4333  exmidsssn  4334  exmidundif  4338  exmidundifim  4339  exmid1stab  4340  pocl  4443  sotritrieq  4465  frirrg  4490  unexg  4584  abnex  4588  reusv3i  4600  ordtriexmid  4663  ontriexmidim  4664  ordtri2orexmid  4665  preleq  4697  0elsucexmid  4707  ordpwsucexmid  4712  ordtri2or2exmid  4713  elomssom  4747  brrelex12  4808  0nelrel  4816  elrel  4872  xpssres  5093  elres  5094  coi2  5299  iotabi  5342  uniabio  5343  nfunv  5405  funun  5417  funcnv3  5438  funimass1  5453  imain  5458  funssxp  5552  f0dom0  5581  f1o00  5671  fsn2  5873  funopsn  5882  isoselem  6016  oprabid  6107  brabvv  6124  uchoice  6361  oprssdmm  6395  1stdm  6406  f1o2ndf1  6454  poxp  6458  suppval1  6469  funsssuppss  6488  rdgon  6647  frecfcllem  6665  nntri3or  6756  nntri1  6759  ensym  7058  en2  7102  xpen  7135  snnen2oprc  7151  phplem4on  7159  fict  7160  fidceq  7161  infiexmid  7171  php5fin  7176  fisbth  7177  fin0  7179  fin0or  7180  diffisn  7187  infnfi  7189  fidcen  7193  en2eqpr  7204  exmidpw  7205  exmidpweq  7206  pw1fin  7207  fientri3  7212  unsnfi  7216  unsnfidcex  7217  unsnfidcel  7218  undifdcss  7220  ssfidc  7235  relcnvfi  7245  fiuni  7302  eqinfti  7350  djulclb  7385  updjud  7412  omp1eomlem  7424  0ct  7437  ctmlemr  7438  ctssdclemn0  7440  ctssdccl  7441  enomnilem  7468  finomni  7470  exmidomni  7472  enmkvlem  7491  enwomnilem  7499  exmidontriimlem1  7567  onntri35  7586  onntri52  7593  dftap2  7607  exmidapne  7616  enq0sym  7789  enq0tr  7791  prarloclem3  7854  nqprl  7908  nqpru  7909  addnqprlemrl  7914  addnqprlemru  7915  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemrl  7930  mulnqprlemru  7931  mulnqprlemfl  7932  mulnqprlemfu  7933  ltexprlemfl  7966  ltexprlemfu  7968  recexprlemopl  7982  recexprlemopu  7984  aptipr  7998  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemladdfu  8034  caucvgprprlemexbt  8063  suplocexprlemrl  8074  suplocexprlemru  8076  suplocexprlemex  8079  srpospr  8140  elrealeu  8186  axarch  8248  axcaucvglemres  8256  nn0ge2m1nn  9606  elnn0z  9636  peano2z  9659  uzm1  9932  qapne  10018  rpregt0  10047  rpnegap  10066  xnn0dcle  10183  xnn0letri  10184  npnflt  10196  nmnfgt  10199  xaddf  10225  xaddval  10226  xltadd1  10257  xsubge0  10262  xleaddadd  10268  elfz1end  10439  1fv  10524  elfzonlteqm1  10606  qtri3or  10653  exbtwnzlemshrink  10661  rebtwn2zlemshrink  10666  ioom  10673  elicore  10679  modfzo0difsn  10810  modsumfzodifsn  10811  addmodlteq  10813  frecfzennn  10841  seq3f1olemstep  10929  ser0  10948  exp3vallem  10955  facp1  11146  faclbnd  11157  bcn1  11174  hashennnuni  11196  hashcl  11198  hashfz1  11200  hashen  11201  fihashdom  11221  hashun  11223  zfz1isolem1  11270  zfz1iso  11271  lencl  11286  sswrd  11291  swrdswrd  11455  swrdccatin2  11479  pfxccat3  11484  pfxccatpfx1  11486  sqrt0  11748  resqrexlemfp1  11753  cau3lem  11858  xrmaxifle  11990  xrmaxiflemval  11994  xrmaxltsup  12002  xrmaxadd  12005  climserle  12089  climcaucn  12095  iserabs  12220  isumshft  12235  cvgratgt0  12278  mertenslem2  12281  prodf1  12287  fprodunsn  12349  fprodfac  12360  eirrap  12523  bezoutlemzz  12757  dfgcd3  12765  nnmindc  12789  nnminle  12790  nninfctlemfo  12795  lcmcllem  12823  prmind2  12876  prm2orodd  12882  sqrt2irr0  12920  sqrt2irrap  12936  ballotfilem2  13206  ballotfilemic  13228  ballotfilem1c  13229  ennnfonelemjn  13271  ennnfonelemdm  13289  ennnfonelemim  13293  ctiunctlemfo  13308  isstructr  13345  basmex  13390  dfgrp2  13809  dfgrp3mlem  13880  mulgnngzsum  13907  grpissubg  13974  ablsubsub23  14106  gsumvalfi  14129  opprringb  14359  rrgmex  14542  aprprop  14574  lssmex  14664  lidlmex  14784  2idlmex  14810  df2idl2  14818  2idlss  14823  isbasis3g  15070  innei  15187  cnpnei  15243  cncnp2m  15255  cnptopresti  15262  cnptoprest2  15264  imasnopn  15323  xmettx  15534  cdivcncfap  15628  expcncf  15633  cnopnap  15635  ivthinclemdisj  15664  dvrecap  15737  dvmptfsum  15749  logfac  15918  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  2lgslem1c  16123  2sqlem10  16158  lfgredg2dom  16287  ausgrusgrben  16323  ausgrumgrien  16325  ausgrusgrien  16326  uspgredg2vlem  16375  uspgredg2v  16376  usgredg2vlem2  16378  ushgredgedg  16381  ushgredgedgloop  16383  griedg0ssusgr  16406  vtxedgfi  16444  vtxlpfi  16445  wlk1walkdom  16514  wlk0prc  16527  clwwlknonex2  16594  eupthi  16604  ex-ceil  16654  bj-nnbist  16686  bj-con1st  16693  bj-charfunbi  16751  bj-sucexg  16862  bj-om  16877  bj-inf2vnlem1  16910  trilpolemisumle  16992  cndcap  17014