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  763  pm2.32  770  oranim  782  stabnot  834  exmiddc  837  pm2.1dc  838  stdcndcOLD  847  stdcn  848  const  853  imanst  889  pm5.75  964  rnlem  978  simp1bi  1014  simp2bi  1015  simp3bi  1016  syl3an1b  1285  syl3an2b  1286  syl3an3b  1287  exalim  1524  nford  1589  nfal  1598  stdpc5  1606  sbbii  1787  sb9i  2007  eu5  2100  exmoeudc  2116  eqeq1  2211  eleq2  2268  nner  2379  rexalim  2498  gencbvex  2818  gencbval  2820  moeq  2947  euind  2959  reuind  2977  ssel  3186  ssrmof  3255  unssd  3348  ssind  3396  unssdif  3407  ss0  3500  prprc  3742  disjnim  4034  trint  4156  snexprc  4229  undifexmid  4236  exmidn0m  4244  exmidsssn  4245  exmidundif  4249  exmidundifim  4250  exmid1stab  4251  pocl  4349  sotritrieq  4371  frirrg  4396  unexg  4489  abnex  4493  reusv3i  4505  ordtriexmid  4568  ontriexmidim  4569  ordtri2orexmid  4570  preleq  4602  0elsucexmid  4612  ordpwsucexmid  4617  ordtri2or2exmid  4618  elomssom  4652  brrelex12  4712  0nelrel  4720  elrel  4776  xpssres  4993  elres  4994  coi2  5198  iotabi  5240  uniabio  5241  nfunv  5303  funun  5314  funcnv3  5335  funimass1  5350  imain  5355  funssxp  5444  f0dom0  5468  f1o00  5556  fsn2  5753  funopsn  5761  isoselem  5888  oprabid  5975  brabvv  5990  uchoice  6222  oprssdmm  6256  1stdm  6267  f1o2ndf1  6313  poxp  6317  rdgon  6471  frecfcllem  6489  nntri3or  6578  nntri1  6581  ensym  6872  en2  6911  xpen  6941  snnen2oprc  6956  phplem4on  6963  fict  6964  fidceq  6965  infiexmid  6973  php5fin  6978  fisbth  6979  fin0  6981  fin0or  6982  diffisn  6989  infnfi  6991  en2eqpr  7003  exmidpw  7004  exmidpweq  7005  pw1fin  7006  fientri3  7011  unsnfi  7015  unsnfidcex  7016  unsnfidcel  7017  undifdcss  7019  ssfidc  7033  relcnvfi  7042  fiuni  7079  eqinfti  7121  djulclb  7156  updjud  7183  omp1eomlem  7195  0ct  7208  ctmlemr  7209  ctssdclemn0  7211  ctssdccl  7212  enomnilem  7239  finomni  7241  exmidomni  7243  enmkvlem  7262  enwomnilem  7270  exmidontriimlem1  7332  onntri35  7348  onntri52  7355  dftap2  7362  exmidapne  7371  enq0sym  7544  enq0tr  7546  prarloclem3  7609  nqprl  7663  nqpru  7664  addnqprlemrl  7669  addnqprlemru  7670  addnqprlemfl  7671  addnqprlemfu  7672  mulnqprlemrl  7685  mulnqprlemru  7686  mulnqprlemfl  7687  mulnqprlemfu  7688  ltexprlemfl  7721  ltexprlemfu  7723  recexprlemopl  7737  recexprlemopu  7739  aptipr  7753  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  caucvgprlemladdfu  7789  caucvgprprlemexbt  7818  suplocexprlemrl  7829  suplocexprlemru  7831  suplocexprlemex  7834  srpospr  7895  elrealeu  7941  axarch  8003  axcaucvglemres  8011  nn0ge2m1nn  9354  elnn0z  9384  peano2z  9407  uzm1  9678  qapne  9759  rpregt0  9788  rpnegap  9807  xnn0dcle  9923  xnn0letri  9924  npnflt  9936  nmnfgt  9939  xaddf  9965  xaddval  9966  xltadd1  9997  xsubge0  10002  xleaddadd  10008  elfz1end  10176  1fv  10260  elfzonlteqm1  10337  qtri3or  10381  exbtwnzlemshrink  10389  rebtwn2zlemshrink  10394  ioom  10401  elicore  10407  modfzo0difsn  10538  modsumfzodifsn  10539  addmodlteq  10541  frecfzennn  10569  seq3f1olemstep  10657  ser0  10676  exp3vallem  10683  facp1  10873  faclbnd  10884  bcn1  10901  hashennnuni  10922  hashcl  10924  hashfz1  10926  hashen  10927  fihashdom  10946  hashun  10948  zfz1isolem1  10983  zfz1iso  10984  lencl  10996  sswrd  11001  sqrt0  11286  resqrexlemfp1  11291  cau3lem  11396  xrmaxifle  11528  xrmaxiflemval  11532  xrmaxltsup  11540  xrmaxadd  11543  climserle  11627  climcaucn  11633  iserabs  11757  isumshft  11772  cvgratgt0  11815  mertenslem2  11818  prodf1  11824  fprodunsn  11886  fprodfac  11897  eirrap  12060  bezoutlemzz  12294  dfgcd3  12302  nnmindc  12326  nnminle  12327  nninfctlemfo  12332  lcmcllem  12360  prmind2  12413  prm2orodd  12419  sqrt2irr0  12457  sqrt2irrap  12473  ennnfonelemjn  12744  ennnfonelemdm  12762  ennnfonelemim  12766  ctiunctlemfo  12781  isstructr  12818  basmex  12862  dfgrp2  13330  dfgrp3mlem  13401  mulgnngsum  13434  grpissubg  13501  ablsubsub23  13632  rrgmex  13994  lssmex  14088  lidlmex  14208  2idlmex  14234  df2idl2  14242  2idlss  14247  isbasis3g  14489  innei  14606  cnpnei  14662  cncnp2m  14674  cnptopresti  14681  cnptoprest2  14683  imasnopn  14742  xmettx  14953  cdivcncfap  15047  expcncf  15052  cnopnap  15054  ivthinclemdisj  15083  dvrecap  15156  dvmptfsum  15168  gausslemma2dlem0i  15505  gausslemma2dlem1a  15506  2lgslem1c  15538  2sqlem10  15573  ex-ceil  15624  bj-nnbist  15642  bj-con1st  15649  bj-charfunbi  15709  bj-sucexg  15820  bj-om  15835  bj-inf2vnlem1  15868  trilpolemisumle  15939  cndcap  15960