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  1526  nford  1591  nfal  1600  stdpc5  1608  sbbii  1789  sb9i  2009  eu5  2103  exmoeudc  2119  eqeq1  2214  eleq2  2271  nner  2382  rexalim  2501  gencbvex  2824  gencbval  2826  moeq  2955  euind  2967  reuind  2985  ssel  3195  ssrmof  3264  unssd  3357  ssind  3405  unssdif  3416  ss0  3509  prprc  3753  disjnim  4049  trint  4173  snexprc  4246  undifexmid  4253  exmidn0m  4261  exmidsssn  4262  exmidundif  4266  exmidundifim  4267  exmid1stab  4268  pocl  4368  sotritrieq  4390  frirrg  4415  unexg  4508  abnex  4512  reusv3i  4524  ordtriexmid  4587  ontriexmidim  4588  ordtri2orexmid  4589  preleq  4621  0elsucexmid  4631  ordpwsucexmid  4636  ordtri2or2exmid  4637  elomssom  4671  brrelex12  4731  0nelrel  4739  elrel  4795  xpssres  5013  elres  5014  coi2  5218  iotabi  5260  uniabio  5261  nfunv  5323  funun  5334  funcnv3  5355  funimass1  5370  imain  5375  funssxp  5465  f0dom0  5491  f1o00  5580  fsn2  5777  funopsn  5785  isoselem  5912  oprabid  5999  brabvv  6014  uchoice  6246  oprssdmm  6280  1stdm  6291  f1o2ndf1  6337  poxp  6341  rdgon  6495  frecfcllem  6513  nntri3or  6602  nntri1  6605  ensym  6896  en2  6936  xpen  6967  snnen2oprc  6982  phplem4on  6990  fict  6991  fidceq  6992  infiexmid  7000  php5fin  7005  fisbth  7006  fin0  7008  fin0or  7009  diffisn  7016  infnfi  7018  en2eqpr  7030  exmidpw  7031  exmidpweq  7032  pw1fin  7033  fientri3  7038  unsnfi  7042  unsnfidcex  7043  unsnfidcel  7044  undifdcss  7046  ssfidc  7060  relcnvfi  7069  fiuni  7106  eqinfti  7148  djulclb  7183  updjud  7210  omp1eomlem  7222  0ct  7235  ctmlemr  7236  ctssdclemn0  7238  ctssdccl  7239  enomnilem  7266  finomni  7268  exmidomni  7270  enmkvlem  7289  enwomnilem  7297  exmidontriimlem1  7364  onntri35  7383  onntri52  7390  dftap2  7398  exmidapne  7407  enq0sym  7580  enq0tr  7582  prarloclem3  7645  nqprl  7699  nqpru  7700  addnqprlemrl  7705  addnqprlemru  7706  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemrl  7721  mulnqprlemru  7722  mulnqprlemfl  7723  mulnqprlemfu  7724  ltexprlemfl  7757  ltexprlemfu  7759  recexprlemopl  7773  recexprlemopu  7775  aptipr  7789  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  caucvgprlemladdfu  7825  caucvgprprlemexbt  7854  suplocexprlemrl  7865  suplocexprlemru  7867  suplocexprlemex  7870  srpospr  7931  elrealeu  7977  axarch  8039  axcaucvglemres  8047  nn0ge2m1nn  9390  elnn0z  9420  peano2z  9443  uzm1  9714  qapne  9795  rpregt0  9824  rpnegap  9843  xnn0dcle  9959  xnn0letri  9960  npnflt  9972  nmnfgt  9975  xaddf  10001  xaddval  10002  xltadd1  10033  xsubge0  10038  xleaddadd  10044  elfz1end  10212  1fv  10296  elfzonlteqm1  10376  qtri3or  10420  exbtwnzlemshrink  10428  rebtwn2zlemshrink  10433  ioom  10440  elicore  10446  modfzo0difsn  10577  modsumfzodifsn  10578  addmodlteq  10580  frecfzennn  10608  seq3f1olemstep  10696  ser0  10715  exp3vallem  10722  facp1  10912  faclbnd  10923  bcn1  10940  hashennnuni  10961  hashcl  10963  hashfz1  10965  hashen  10966  fihashdom  10985  hashun  10987  zfz1isolem1  11022  zfz1iso  11023  lencl  11035  sswrd  11040  swrdswrd  11196  swrdccatin2  11220  pfxccat3  11225  pfxccatpfx1  11227  sqrt0  11430  resqrexlemfp1  11435  cau3lem  11540  xrmaxifle  11672  xrmaxiflemval  11676  xrmaxltsup  11684  xrmaxadd  11687  climserle  11771  climcaucn  11777  iserabs  11901  isumshft  11916  cvgratgt0  11959  mertenslem2  11962  prodf1  11968  fprodunsn  12030  fprodfac  12041  eirrap  12204  bezoutlemzz  12438  dfgcd3  12446  nnmindc  12470  nnminle  12471  nninfctlemfo  12476  lcmcllem  12504  prmind2  12557  prm2orodd  12563  sqrt2irr0  12601  sqrt2irrap  12617  ennnfonelemjn  12888  ennnfonelemdm  12906  ennnfonelemim  12910  ctiunctlemfo  12925  isstructr  12962  basmex  13006  dfgrp2  13474  dfgrp3mlem  13545  mulgnngsum  13578  grpissubg  13645  ablsubsub23  13776  rrgmex  14138  lssmex  14232  lidlmex  14352  2idlmex  14378  df2idl2  14386  2idlss  14391  isbasis3g  14633  innei  14750  cnpnei  14806  cncnp2m  14818  cnptopresti  14825  cnptoprest2  14827  imasnopn  14886  xmettx  15097  cdivcncfap  15191  expcncf  15196  cnopnap  15198  ivthinclemdisj  15227  dvrecap  15300  dvmptfsum  15312  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  2lgslem1c  15682  2sqlem10  15717  lfgredg2dom  15838  ex-ceil  15862  bj-nnbist  15880  bj-con1st  15887  bj-charfunbi  15946  bj-sucexg  16057  bj-om  16072  bj-inf2vnlem1  16105  trilpolemisumle  16179  cndcap  16200