Theorem biimpi 119

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		bi1 117	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbi  120  sylib  121  sylbb  122  biimpri  132  mpbi  144  syl5bi  151  syl6ib  160  syl7bi  164  syl8ib  165  bitri  183  simplbi  272  simprbi  273  sylanb  282  sylan2b  285  anc2l  325  sylanblc  412  orbi2i  752  pm2.32  759  oranim  771  stabnot  819  exmiddc  822  pm2.1dc  823  stdcndcOLD  832  stdcn  833  imanst  874  pm5.75  947  rnlem  961  simp1bi  997  simp2bi  998  simp3bi  999  syl3an1b  1253  syl3an2b  1254  syl3an3b  1255  exalim  1479  nford  1547  stdpc5  1564  sbbii  1739  sb9i  1956  eu5  2047  exmoeudc  2063  eqeq1  2147  eleq2  2204  nner  2313  rexalim  2431  gencbvex  2735  gencbval  2737  moeq  2863  euind  2875  reuind  2893  ssel  3096  ssrmof  3165  unssd  3257  ssind  3305  unssdif  3316  ss0  3408  prprc  3641  disjnim  3928  trint  4049  snexprc  4118  undifexmid  4125  exmidn0m  4132  exmidsssn  4133  exmidundif  4137  exmidundifim  4138  pocl  4233  sotritrieq  4255  frirrg  4280  unexg  4372  abnex  4376  reusv3i  4388  ordtriexmid  4445  ordtri2orexmid  4446  preleq  4478  0elsucexmid  4488  ordpwsucexmid  4493  ordtri2or2exmid  4494  elnn  4527  brrelex12  4585  0nelrel  4593  elrel  4649  xpssres  4862  elres  4863  coi2  5063  iotabi  5105  uniabio  5106  nfunv  5164  funun  5175  funcnv3  5193  funimass1  5208  imain  5213  funssxp  5300  f0dom0  5324  f1o00  5410  fsn2  5602  isoselem  5729  oprabid  5811  brabvv  5825  oprssdmm  6077  1stdm  6088  f1o2ndf1  6133  poxp  6137  rdgon  6291  frecfcllem  6309  nntri3or  6397  nntri1  6400  ensym  6683  xpen  6747  snnen2oprc  6762  phplem4on  6769  fict  6770  fidceq  6771  infiexmid  6779  php5fin  6784  fisbth  6785  fin0  6787  fin0or  6788  diffisn  6795  infnfi  6797  en2eqpr  6809  exmidpw  6810  fientri3  6811  unsnfi  6815  unsnfidcex  6816  unsnfidcel  6817  undifdcss  6819  ssfidc  6831  relcnvfi  6837  fiuni  6874  eqinfti  6915  djulclb  6948  updjud  6975  omp1eomlem  6987  0ct  7000  ctmlemr  7001  ctssdclemn0  7003  ctssdccl  7004  enomnilem  7018  finomni  7020  exmidomni  7022  enmkvlem  7043  enwomnilem  7050  enq0sym  7264  enq0tr  7266  prarloclem3  7329  nqprl  7383  nqpru  7384  addnqprlemrl  7389  addnqprlemru  7390  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemrl  7405  mulnqprlemru  7406  mulnqprlemfl  7407  mulnqprlemfu  7408  ltexprlemfl  7441  ltexprlemfu  7443  recexprlemopl  7457  recexprlemopu  7459  aptipr  7473  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  caucvgprlemladdfu  7509  caucvgprprlemexbt  7538  suplocexprlemrl  7549  suplocexprlemru  7551  suplocexprlemex  7554  srpospr  7615  elrealeu  7661  axarch  7723  axcaucvglemres  7731  nn0ge2m1nn  9061  elnn0z  9091  peano2z  9114  uzm1  9380  qapne  9458  rpregt0  9484  rpnegap  9503  npnflt  9628  nmnfgt  9631  xaddf  9657  xaddval  9658  xltadd1  9689  xsubge0  9694  xleaddadd  9700  elfz1end  9866  1fv  9947  elfzonlteqm1  10018  qtri3or  10051  exbtwnzlemshrink  10057  rebtwn2zlemshrink  10062  ioom  10069  modfzo0difsn  10199  modsumfzodifsn  10200  addmodlteq  10202  frecfzennn  10230  seq3f1olemstep  10305  ser0  10318  exp3vallem  10325  facp1  10508  faclbnd  10519  bcn1  10536  hashennnuni  10557  hashcl  10559  hashfz1  10561  hashen  10562  fihashdom  10581  hashun  10583  zfz1isolem1  10615  zfz1iso  10616  sqrt0  10808  resqrexlemfp1  10813  cau3lem  10918  xrmaxifle  11047  xrmaxiflemval  11051  xrmaxltsup  11059  xrmaxadd  11062  climserle  11146  climcaucn  11152  iserabs  11276  isumshft  11291  cvgratgt0  11334  mertenslem2  11337  prodf1  11343  eirrap  11520  bezoutlemzz  11726  dfgcd3  11734  lcmcllem  11784  prmind2  11837  prm2orodd  11843  sqrt2irr0  11878  sqrt2irrap  11894  ennnfonelemjn  11951  ennnfonelemdm  11969  ennnfonelemim  11973  ctiunctlemfo  11988  isstructr  12013  isbasis3g  12252  innei  12371  cnpnei  12427  cncnp2m  12439  cnptopresti  12446  cnptoprest2  12448  imasnopn  12507  xmettx  12718  cdivcncfap  12795  expcncf  12800  cnopnap  12802  ivthinclemdisj  12826  dvrecap  12885  ex-ceil  13109  bj-nnbist  13124  bj-sucexg  13291  bj-om  13306  bj-inf2vnlem1  13339  exmid1stab  13368  trilpolemisumle  13406