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  411  orbi2i  751  pm2.32  758  oranim  770  stabnot  818  exmiddc  821  pm2.1dc  822  stdcndcOLD  831  stdcn  832  imanst  873  pm5.75  946  rnlem  960  simp1bi  996  simp2bi  997  simp3bi  998  syl3an1b  1252  syl3an2b  1253  syl3an3b  1254  exalim  1478  nford  1546  stdpc5  1563  sbbii  1738  sb9i  1955  eu5  2046  exmoeudc  2062  eqeq1  2146  eleq2  2203  nner  2312  rexalim  2430  gencbvex  2732  gencbval  2734  moeq  2859  euind  2871  reuind  2889  ssel  3091  ssrmof  3160  unssd  3252  ssind  3300  unssdif  3311  ss0  3403  prprc  3633  disjnim  3920  trint  4041  snexprc  4110  undifexmid  4117  exmidn0m  4124  exmidsssn  4125  exmidundif  4129  exmidundifim  4130  pocl  4225  sotritrieq  4247  frirrg  4272  unexg  4364  abnex  4368  reusv3i  4380  ordtriexmid  4437  ordtri2orexmid  4438  preleq  4470  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  elnn  4519  brrelex12  4577  0nelrel  4585  elrel  4641  xpssres  4854  elres  4855  coi2  5055  iotabi  5097  uniabio  5098  nfunv  5156  funun  5167  funcnv3  5185  funimass1  5200  imain  5205  funssxp  5292  f0dom0  5316  f1o00  5402  fsn2  5594  isoselem  5721  oprabid  5803  brabvv  5817  oprssdmm  6069  1stdm  6080  f1o2ndf1  6125  poxp  6129  rdgon  6283  frecfcllem  6301  nntri3or  6389  nntri1  6392  ensym  6675  xpen  6739  snnen2oprc  6754  phplem4on  6761  fict  6762  fidceq  6763  infiexmid  6771  php5fin  6776  fisbth  6777  fin0  6779  fin0or  6780  diffisn  6787  infnfi  6789  en2eqpr  6801  exmidpw  6802  fientri3  6803  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  undifdcss  6811  ssfidc  6823  relcnvfi  6829  fiuni  6866  eqinfti  6907  djulclb  6940  updjud  6967  omp1eomlem  6979  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdccl  6996  enomnilem  7010  finomni  7012  exmidomni  7014  enq0sym  7240  enq0tr  7242  prarloclem3  7305  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemrl  7381  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  ltexprlemfl  7417  ltexprlemfu  7419  recexprlemopl  7433  recexprlemopu  7435  aptipr  7449  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  caucvgprlemladdfu  7485  caucvgprprlemexbt  7514  suplocexprlemrl  7525  suplocexprlemru  7527  suplocexprlemex  7530  srpospr  7591  elrealeu  7637  axarch  7699  axcaucvglemres  7707  nn0ge2m1nn  9037  elnn0z  9067  peano2z  9090  uzm1  9356  qapne  9431  rpregt0  9455  rpnegap  9474  npnflt  9598  nmnfgt  9601  xaddf  9627  xaddval  9628  xltadd1  9659  xsubge0  9664  xleaddadd  9670  elfz1end  9835  1fv  9916  elfzonlteqm1  9987  qtri3or  10020  exbtwnzlemshrink  10026  rebtwn2zlemshrink  10031  ioom  10038  modfzo0difsn  10168  modsumfzodifsn  10169  addmodlteq  10171  frecfzennn  10199  seq3f1olemstep  10274  ser0  10287  exp3vallem  10294  facp1  10476  faclbnd  10487  bcn1  10504  hashennnuni  10525  hashcl  10527  hashfz1  10529  hashen  10530  fihashdom  10549  hashun  10551  zfz1isolem1  10583  zfz1iso  10584  sqrt0  10776  resqrexlemfp1  10781  cau3lem  10886  xrmaxifle  11015  xrmaxiflemval  11019  xrmaxltsup  11027  xrmaxadd  11030  climserle  11114  climcaucn  11120  iserabs  11244  isumshft  11259  cvgratgt0  11302  mertenslem2  11305  prodf1  11311  eirrap  11484  bezoutlemzz  11690  dfgcd3  11698  lcmcllem  11748  prmind2  11801  prm2orodd  11807  sqrt2irr0  11842  sqrt2irrap  11858  ennnfonelemjn  11915  ennnfonelemdm  11933  ennnfonelemim  11937  ctiunctlemfo  11952  isstructr  11974  isbasis3g  12213  innei  12332  cnpnei  12388  cncnp2m  12400  cnptopresti  12407  cnptoprest2  12409  imasnopn  12468  xmettx  12679  cdivcncfap  12756  expcncf  12761  cnopnap  12763  ivthinclemdisj  12787  dvrecap  12846  ex-ceil  12938  bj-nnbist  12953  bj-sucexg  13120  bj-om  13135  bj-inf2vnlem1  13168  exmid1stab  13195  trilpolemisumle  13231