Theorem biimpri 228

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 220. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)

Hypothesis

Ref	Expression
biimpri.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
biimpri	⊢ (𝜓 → 𝜑)

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	bicomi 224	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 216	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  mpbir  231  sylibr  234  sylbir  235  sylbbr  236  sylbb1  237  sylbb2  238  biimtrrid  243  imbitrrdi  252  mtbi  322  sylnib  328  simplbi2  500  sylanbr  581  sylan2br  594  pm2.54  851  orbi2i  911  pm2.31  921  pm2.85  931  pm3.11  993  syl3an1br  1406  syl3an2br  1407  syl3an3br  1408  had1  1600  nic-axALT  1672  speimfw  1963  sbbii  2076  hbsbwOLD  2173  mobii  2551  mo4  2569  nfabdwOLD  2933  r19.30  3126  r19.30OLD  3127  ceqsexv2dOLD  3546  eueq2  3732  ralun  4221  ssunieq  4967  ax6vsep  5321  opelxpi  5737  ordunidif  6444  unizlim  6518  dffo2  6838  dff1o2  6867  resdif  6883  f1o00  6897  fvimacnvALT  7090  fvcofneq  7127  exfo  7139  ressnop0  7187  fsnunfv  7221  ovid  7591  ovidig  7592  dfwe2  7809  dford5  7819  onminex  7838  nnsuc  7921  1stnpr  8034  2ndnpr  8035  f1stres  8054  f2ndres  8055  1st2val  8058  2nd2val  8059  frxp  8167  soxp  8170  frxp2  8185  fprlem1  8341  tz7.49  8501  elixpsn  8995  domdifsn  9120  domunsncan  9138  unfi  9238  cnvfi  9243  fineqvlem  9325  unblem4  9359  ordiso2  9584  zfreg  9664  inf3lem3  9699  trcl  9797  unir1  9882  ssrankr1  9904  djuunxp  9990  pm54.43lem  10069  infxpenlem  10082  ween  10104  acni3  10116  kmlem1  10220  infdif  10277  ackbij1lem1  10288  fin23lem32  10413  isfin1-3  10455  axdc3lem2  10520  ac6c4  10550  zornn0g  10574  axdclem2  10589  rnct  10594  brdom3  10597  brdom5  10598  brdom4  10599  brdom6disj  10601  konigthlem  10637  pwcfsdom  10652  cfpwsdom  10653  alephom  10654  gruina  10887  grur1  10889  grothomex  10898  grothac  10899  nqpr  11083  axcnre  11233  axpre-sup  11238  ssxr  11359  le2tri3i  11420  muldivdir  11987  0nn0  12568  uzind4  12971  rpnnen1lem5  13046  elfz4  13577  eluzfz  13579  ssfzo12bi  13811  fzoopth  13812  hashgt0elex  14450  hashgt23el  14473  hashxplem  14482  hashfun  14486  ishashinf  14512  wrdsymb1  14601  ccatfv0  14631  lswccats1fst  14683  ccatswrd  14716  ccatpfx  14749  splfv1  14803  repswfsts  14829  cshinj  14859  swrdco  14886  cotr2g  15025  trclun  15063  resqrex  15299  sumeven  16435  ndvdsadd  16458  gcdcllem1  16545  gcdcllem3  16547  lcmftp  16683  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  lcmfun  16692  coprmprod  16708  coprmproddvdslem  16709  divgcdcoprmex  16713  1idssfct  16727  prmodvdslcmf  17094  cshwrepswhash1  17150  xpsfrnel2  17624  xpsff1o  17627  catcone0  17745  initoeu2  18083  clatlem  18572  clatlubcl2  18574  clatglbcl2  18576  xpsmnd  18812  xpsgrp  19099  mulgfval  19109  gsmsymgrfix  19470  pmtr3ncom  19517  gsumcom3fi  20021  dprdfeq0  20066  gsumdixp  20342  lspcl  20997  lindfind  21859  lindsind  21860  lindsind2  21862  lindff1  21863  f1linds  21868  evls1maplmhm  22402  mat1dimscm  22502  mdetunilem7  22645  fvmptnn04if  22876  tgcl  22997  elcls  23102  opnnei  23149  neiptopnei  23161  cnpnei  23293  cmpfii  23438  txcnp  23649  xpstps  23839  fbun  23869  isfild  23887  snfil  23893  filconn  23912  isufil2  23937  hauspwpwf1  24016  cnextcn  24096  ustfilxp  24242  ustuqtop4  24274  xpsxms  24568  xpsms  24569  rlmnvc  24745  nmoid  24784  xrsmopn  24853  xrhmeo  24996  cphsqrtcl  25237  iscmet3  25346  iundisj  25602  ioorinv  25630  bddiblnc  25897  dvtaylp  26430  logbid1  26829  logbchbase  26832  relogbcxpb  26848  logbmpt  26849  logbfval  26851  musum  27252  lgsmodeq  27404  lgsmulsqcoprm  27405  2lgs  27469  2sqnn0  27500  pntlem3  27671  sltval2  27719  noxp1o  27726  conway  27862  scutbdaylt  27881  nbupgrel  29380  nbusgrvtxm1  29414  nb3gr2nb  29419  pthdivtx  29765  pthdlem2lem  29803  crctisclwlk  29830  wwlks  29868  wwlksonvtx  29888  wspthnonp  29892  wlkiswwlks2lem1  29902  wwlksnndef  29938  wwlksnfi  29939  clwlkclwwlkf1lem3  30038  clwlkclwwlkf1  30042  clwwlknnn  30065  clwwlkel  30078  clwwlkf1  30081  wwlksext2clwwlk  30089  clwwlknonwwlknonb  30138  umgr3v3e3cycl  30216  frgrncvvdeq  30341  sspval  30755  blo3i  30834  ajfval  30841  spanval  31365  cmcmlem  31623  leopnmid  32170  csmdsymi  32366  chirredlem4  32425  sumdmdlem  32450  iundisjf  32611  padct  32733  iundisjfi  32801  nn0difffzod  32811  hashxpe  32814  fprodex01  32829  xrpxdivcld  32899  fldgensdrg  33281  lsmsnorb  33384  mxidlnzr  33460  zringfrac  33547  lactlmhm  33647  extdgval  33667  ccfldextdgrr  33682  ply1annprmidl  33700  pnfneige0  33897  rrhre  33967  esumcocn  34044  hasheuni  34049  sgon  34088  sigapildsys  34126  ddemeas  34200  dya2iocct  34245  dya2iocnrect  34246  eulerpartgbij  34337  eulerpartlemgs2  34345  coinflippv  34448  signstfvneq0  34549  hgt750lemb  34633  bnj1136  34973  bnj1175  34980  bnj1408  35012  fnrelpredd  35065  pthhashvtx  35095  spthcycl  35097  upgracycumgr  35121  umgracycusgr  35122  cvmsdisj  35238  mrsubvrs  35490  mppspstlem  35539  problem4  35636  climuzcnv  35639  currybi  35656  dfon2lem7  35753  imageval  35894  filnetlem2  36345  df3nandALT1  36365  lukshef-ax2  36381  arg-ax  36382  weiunpo  36431  bj-andnotim  36554  bj-modalbe  36654  bj-hbs1  36778  bj-hbsb2av  36780  bj-2uplex  36988  mptsnunlem  37304  onsucuni3  37333  fvineqsneq  37378  finixpnum  37565  fin2solem  37566  matunitlindflem2  37577  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  poimirlem32  37612  mblfinlem3  37619  itg2addnclem2  37632  itg2addnc  37634  ftc1anclem6  37658  heiborlem3  37773  ismndo2  37834  rngomndo  37895  isfld2  37965  isfldidl  38028  dmncan2  38037  oprabbi  38121  opabbi  38125  ac6s3f  38131  relcnveq3  38277  elrelscnveq3  38447  lsat0cv  38989  pclfinclN  39907  docavalN  41080  djavalN  41092  dochval  41308  djhval  41355  dochexmidlem8  41424  dochkr1  41435  dochkr1OLDN  41436  hdmap1fval  41753  lcmineqlem13  41998  unitscyglem4  42155  fiabv  42491  selvcllem5  42537  mhpind  42549  pellexlem5  42789  rmyabs  42915  jm2.24  42920  islssfgi  43029  pwslnm  43051  dgraaub  43105  omlimcl2  43203  onexoegt  43205  rp-oelim2  43270  oeord2lim  43271  oeord2i  43272  ensucne0OLD  43492  iscard5  43498  clrellem  43584  frege114d  43720  frege55lem1a  43828  frege70  43895  gneispace  44096  ismnushort  44270  3impexpbicom  44450  ee3bir  44474  vk15.4j  44499  onfrALTlem2  44517  ax6e2nd  44529  dfvd1impr  44547  dfvd2impr  44575  e1bir  44601  e2bir  44604  e3bir  44710  suctrALT  44797  19.21a3con13vVD  44823  3impexpbicomVD  44828  tratrbVD  44832  ssralv2VD  44837  truniALTVD  44849  trintALTVD  44851  undif3VD  44853  csbingVD  44855  onfrALTlem3VD  44858  onfrALTlem2VD  44860  onfrALTVD  44862  csbsngVD  44864  csbxpgVD  44865  csbrngVD  44867  csbunigVD  44869  csbfv12gALTVD  44870  relopabVD  44872  ax6e2ndVD  44879  2uasbanhVD  44882  vk15.4jVD  44885  sspwimp  44889  sspwimpVD  44890  sspwimpcf  44891  sspwimpcfVD  44892  suctrALTcf  44893  suctrALTcfVD  44894  suctrALT3  44895  sspwimpALT  44896  unisnALT  44897  ax6e2ndALT  44901  isosctrlem1ALT  44905  iunconnlem2  44906  supminfxrrnmpt  45386  limsuppnflem  45631  limsupubuz  45634  cncfuni  45807  iblcncfioo  45899  stoweidlem14  45935  stoweidlem17  45938  stoweidlem35  45956  stoweidlem57  45978  stirlinglem7  46001  stirlinglem10  46004  fourierdlem54  46081  fourierdlem62  46089  fourierdlem63  46090  fourierdlem65  46092  fourierdlem73  46100  fourierdlem80  46107  fourierdlem82  46109  fourierdlem101  46128  etransclem32  46187  ioorrnopnxr  46228  subsaliuncl  46279  meadjiunlem  46386  ismeannd  46388  voliunsge0lem  46393  volmea  46395  caratheodory  46449  ovnsubaddlem2  46492  hoidmvlelem5  46520  hoiqssbllem2  46544  iinhoiicc  46595  aibandbiaiaiffb  46810  funressnvmo  46960  dfdfat2  47043  afvres  47087  tz6.12-afv  47088  ndmaovass  47121  afv2res  47154  tz6.12-afv2  47155  el1fzopredsuc  47240  fundcmpsurinjimaid  47285  iccpartiltu  47296  iccelpart  47307  lswn0  47318  ichnfimlem  47337  prprelb  47390  evenprm2  47588  dfnbgr6  47729  dfsclnbgr6  47730  isgrtri  47794  lincext1  48183  sepfsepc  48607  isclatd  48655  intubeu  48656  unilbeu  48657  fullthinc  48713  setc2othin  48723