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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used 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  3778  prprc  3823  disjnim  4120  trint  4244  snexprc  4323  undifexmid  4330  exmidn0m  4338  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  pocl  4448  sotritrieq  4470  frirrg  4495  unexg  4589  abnex  4593  reusv3i  4605  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  preleq  4702  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  elomssom  4752  brrelex12  4813  0nelrel  4821  elrel  4877  xpssres  5098  elres  5099  coi2  5304  iotabi  5347  uniabio  5348  nfunv  5410  funun  5422  funcnv3  5443  funimass1  5458  imain  5463  funssxp  5557  f0dom0  5586  f1o00  5676  fsn2  5882  funopsn  5891  isoselem  6026  oprabid  6117  brabvv  6134  uchoice  6371  oprssdmm  6405  1stdm  6416  f1o2ndf1  6464  poxp  6468  suppval1  6479  funsssuppss  6498  rdgon  6657  frecfcllem  6675  nntri3or  6766  nntri1  6769  ensym  7068  en2  7112  xpen  7145  snnen2oprc  7161  phplem4on  7169  fict  7170  fidceq  7171  infiexmid  7181  php5fin  7186  fisbth  7187  fin0  7189  fin0or  7190  diffisn  7197  infnfi  7199  fidcen  7203  en2eqpr  7214  exmidpw  7215  exmidpweq  7216  pw1fin  7217  fientri3  7222  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  ssfidc  7245  relcnvfi  7255  fiuni  7312  eqinfti  7360  djulclb  7395  updjud  7422  omp1eomlem  7434  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdccl  7451  enomnilem  7478  finomni  7480  exmidomni  7482  enmkvlem  7501  enwomnilem  7509  exmidontriimlem1  7577  onntri35  7596  onntri52  7603  dftap2  7617  exmidapne  7626  enq0sym  7799  enq0tr  7801  prarloclem3  7864  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  ltexprlemfl  7976  ltexprlemfu  7978  recexprlemopl  7992  recexprlemopu  7994  aptipr  8008  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemladdfu  8044  caucvgprprlemexbt  8073  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemex  8089  srpospr  8150  elrealeu  8196  axarch  8258  axcaucvglemres  8266  nn0ge2m1nn  9631  elnn0z  9661  peano2z  9684  uzm1  9962  qapne  10048  rpregt0  10078  rpnegap  10097  xnn0dcle  10214  xnn0letri  10215  npnflt  10227  nmnfgt  10230  xaddf  10256  xaddval  10257  xltadd1  10288  xsubge0  10293  xleaddadd  10299  elfz1end  10471  1fv  10556  elfzonlteqm1  10638  qtri3or  10685  exbtwnzlemshrink  10693  rebtwn2zlemshrink  10698  ioom  10705  elicore  10711  modfzo0difsn  10845  modsumfzodifsn  10846  addmodlteq  10848  frecfzennn  10876  seq3f1olemstep  10964  ser0  10983  exp3vallem  10990  facp1  11182  faclbnd  11193  bcn1  11210  hashennnuni  11232  hashcl  11234  hashfz1  11236  hashen  11237  fihashdom  11257  hashun  11259  zfz1isolem1  11306  zfz1iso  11307  lencl  11322  sswrd  11327  swrdswrd  11491  swrdccatin2  11515  pfxccat3  11520  pfxccatpfx1  11522  sqrt0  11784  resqrexlemfp1  11789  cau3lem  11895  xrmaxifle  12028  xrmaxiflemval  12032  xrmaxltsup  12040  xrmaxadd  12043  climserle  12127  climcaucn  12133  iserabs  12258  isumshft  12273  cvgratgt0  12316  mertenslem2  12319  prodf1  12325  fprodunsn  12387  fprodfac  12398  eirrap  12561  bezoutlemzz  12795  dfgcd3  12803  nnmindc  12827  nnminle  12828  nninfctlemfo  12833  lcmcllem  12861  prmind2  12914  prm2orodd  12920  sqrt2irr0  12959  sqrt2irrap  12976  ballotfilem2  13277  ballotfilemic  13299  ballotfilem1c  13300  ennnfonelemjn  13342  ennnfonelemdm  13360  ennnfonelemim  13364  ctiunctlemfo  13379  isstructr  13416  basmex  13461  dfgrp2  13881  dfgrp3mlem  13952  mulgnngzsum  13979  grpissubg  14046  ablsubsub23  14178  gsumvalfi  14201  opprringb  14435  rrgmex  14618  aprprop  14650  lssmex  14741  lidlmex  14861  2idlmex  14887  df2idl2  14895  2idlss  14900  isbasis3g  15196  innei  15313  cnpnei  15369  cncnp2m  15381  cnptopresti  15388  cnptoprest2  15390  imasnopn  15449  xmettx  15660  cdivcncfap  15754  expcncf  15759  cnopnap  15761  ivthinclemdisj  15790  dvrecap  15863  dvmptfsum  15875  logfac  16048  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  2lgslem1c  16307  2sqlem10  16342  lfgredg2dom  16471  ausgrusgrben  16507  ausgrumgrien  16509  ausgrusgrien  16510  uspgredg2vlem  16559  uspgredg2v  16560  usgredg2vlem2  16562  ushgredgedg  16565  ushgredgedgloop  16567  griedg0ssusgr  16590  vtxedgfi  16628  vtxlpfi  16629  wlk1walkdom  16698  wlk0prc  16711  clwwlknonex2  16778  eupthi  16788  ex-ceil  16838  bj-nnbist  16870  bj-con1st  16877  bj-charfunbi  16935  bj-sucexg  17046  bj-om  17061  bj-inf2vnlem1  17094  trilpolemisumle  17185  cndcap  17207  als-no-surprise  17245