Theorem biimpri 217

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 209. (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 213	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 205	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  mpbir  220  sylibr  223  sylbir  224  sylbbr  225  sylbb1  226  sylbb2  227  syl5bir  232  syl6ibr  241  mtbi  311  pm2.54  388  sylanbr  489  sylan2br  492  pm3.11  519  orbi2i  540  pm2.31  546  simplbi2  653  dfbi  659  pm2.85  894  pm3.2an3  1233  syl3an1br  1357  syl3an2br  1358  syl3an3br  1359  had1  1533  nic-axALT  1590  speimfw  1863  sbbii  1874  ceqsexv2d  3216  eueq2  3347  ralun  3757  ssunieq  4408  ax6vsep  4713  opelxpi  5072  elsnxpOLD  5595  ordunidif  5690  unizlim  5761  funtpgOLD  5857  dffo2  6032  dff1o2  6055  resdif  6070  f1o00  6083  fvimacnvALT  6244  fvcofneq  6275  exfo  6285  ressnop0  6325  fsnunfv  6358  ovid  6675  ovidig  6676  dfwe2  6873  onminex  6899  nnsuc  6974  1stnpr  7063  2ndnpr  7064  f1stres  7081  f2ndres  7082  1st2val  7085  2nd2val  7086  frxp  7174  soxp  7177  tz7.49  7427  elixpsn  7833  domdifsn  7928  domunsncan  7945  fineqvlem  8059  unblem4  8100  ordiso2  8303  domwdom  8362  zfreg  8383  inf3lem3  8410  trcl  8487  unir1  8559  ssrankr1  8581  pm54.43lem  8708  infxpenlem  8719  ween  8741  acni3  8753  kmlem1  8855  infdif  8914  ackbij1lem1  8925  fin23lem14  9038  fin23lem32  9049  isfin1-3  9091  axcc2lem  9141  axdc3lem2  9156  ac6c4  9186  zornn0g  9210  axdclem2  9225  brdom3  9231  brdom5  9232  brdom4  9233  brdom6disj  9235  konigthlem  9269  pwcfsdom  9284  cfpwsdom  9285  alephom  9286  gruina  9519  grur1  9521  grothomex  9530  grothac  9531  nqpr  9715  axcnre  9864  axpre-sup  9869  ssxr  9986  le2tri3i  10046  muldivdir  10599  0nn0  11184  uzind4  11622  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  elfz4  12206  eluzfz  12208  ssfzo12bi  12429  hashgt0elex  13050  hashxplem  13080  hashfun  13084  ishashinf  13104  ffz0iswrd  13187  wrdsymb1  13197  ccatfv0  13220  lswccats1fst  13264  ccatswrd  13308  repswfsts  13379  cshinj  13408  cshw1  13419  swrdco  13434  cotr2g  13563  xptrrel  13567  trclun  13603  resqrex  13839  pwm1geoser  14439  sumeven  14948  ndvdsadd  14972  gcdcllem1  15059  gcdcllem3  15061  lcmftp  15187  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  lcmfun  15196  ncoprmgcdne1b  15201  coprmprod  15213  coprmproddvdslem  15214  divgcdcoprmex  15218  1idssfct  15231  prmodvdslcmf  15589  cshwrepswhash1  15647  xpsff1o  16051  initoeu2  16489  clatlem  16934  clatlubcl2  16936  clatglbcl2  16938  xpsmnd  17153  sgrp2rid2  17236  xpsgrp  17357  symg2bas  17641  symgextf  17660  gsmsymgrfix  17671  gsmsymgreqlem2  17674  pmtr3ncom  17718  odlem1  17777  gexlem1  17817  dprdfeq0  18244  gsumdixp  18432  lspcl  18797  cply1mul  19485  psgndiflemB  19765  lindfind  19974  lindsind  19975  lindsind2  19977  lindff1  19978  f1linds  19983  gsumcom3fi  20025  mat1dimscm  20100  dmatmul  20122  mdetdiag  20224  mdetunilem7  20243  mdetunilem9  20245  madurid  20269  fvmptnn04if  20473  tgcl  20584  elcls  20687  opnnei  20734  neiptopnei  20746  cnpnei  20878  cmpfii  21022  txcnp  21233  xpstps  21423  fbun  21454  isfild  21472  snfil  21478  filcon  21497  isufil2  21522  hauspwpwf1  21601  cnextcn  21681  ustfilxp  21826  ustuqtop4  21858  xpsxms  22149  xpsms  22150  rlmnvc  22317  nmoid  22356  xrsmopn  22423  xrhmeo  22553  cphsqrtcl  22792  iscmet3  22899  iundisj  23123  ioorinv  23150  plyexmo  23872  aalioulem3  23893  dvtaylp  23928  dvradcnv  23979  logtayllem  24205  logtayl  24206  logbid1  24306  logbchbase  24309  relogbcxpb  24325  logbmpt  24326  logbfval  24328  musum  24717  lgsmodeq  24867  lgsmulsqcoprm  24868  2lgs  24932  pntlem3  25098  upgredg  25811  nb3grapr  25982  nb3grapr2  25983  nb3gra2nb  25984  wlkcpr  26057  2pthlem2  26126  nvnencycllem  26171  wlkiswwlk2lem1  26219  clwwlkel  26321  clwwlkf1  26324  clwlkf1clwwlklem  26376  2wlkonotv  26404  clwlknclwlkdifs  26487  frgra0v  26520  frgra3v  26529  2pthfrgrarn  26536  2pthfrgra  26538  n4cyclfrgra  26545  frgrancvvdeqlem9  26568  frgrawopreglem3  26573  frgraregorufr0  26579  numclwwlk2lem1  26629  sspval  26962  blo3i  27041  ajfval  27048  spanval  27576  cmcmlem  27834  leopnmid  28381  csmdsymi  28577  chirredlem4  28636  sumdmdlem  28661  iundisjf  28784  rnct  28879  padct  28885  iundisjfi  28942  xrpxdivcld  28974  pnfneige0  29325  rrhre  29393  esumcocn  29469  hasheuni  29474  sgon  29514  sigapildsys  29552  ddemeas  29626  1stmbfm  29649  2ndmbfm  29650  dya2iocct  29669  dya2iocnrect  29670  eulerpartgbij  29761  eulerpartlemgs2  29769  coinflippv  29872  bnj1136  30319  bnj1175  30326  bnj1408  30358  cvmsdisj  30506  mrsubvrs  30673  mppspstlem  30722  problem4  30816  climuzcnv  30819  dfon2lem7  30938  sltval2  31053  nodenselem5  31084  imageval  31207  filnetlem2  31544  df3nandALT1  31566  lukshef-ax2  31584  arg-ax  31585  sylancl3  31738  bj-andnotim  31746  bj-modalbe  31865  bj-2uplex  32203  bj-toprntopon  32244  mptsnunlem  32361  onsucuni3  32391  finixpnum  32564  fin2solem  32565  matunitlindflem2  32576  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem32  32611  mblfinlem3  32618  itg2addnclem2  32632  itg2addnc  32634  bddiblnc  32650  ftc1anclem6  32660  heiborlem3  32782  ismndo2  32843  rngomndo  32904  isfld2  32974  isfldidl  33037  dmncan2  33046  oprabbi  33140  opabbi  33144  ac6s3f  33149  lsat0cv  33338  pclfinclN  34254  docavalN  35430  djavalN  35442  dochval  35658  djhval  35705  dochexmidlem8  35774  dochkr1  35785  dochkr1OLDN  35786  hdmap1fval  36104  pellexlem5  36415  rmyabs  36543  jm2.24  36548  islssfgi  36660  pwslnm  36682  dgraaub  36737  clrellem  36948  frege114d  37069  frege55lem1a  37180  frege70  37247  gneispace  37452  3impexpbicom  37706  ee3bir  37730  vk15.4j  37755  onfrALTlem2  37782  ax6e2nd  37795  dfvd1impr  37813  dfvd2impr  37850  e1bir  37876  e2bir  37879  e3bir  37987  suctrALT  38083  19.21a3con13vVD  38109  3impexpbicomVD  38114  tratrbVD  38119  ssralv2VD  38124  truniALTVD  38136  trintALTVD  38138  undif3VD  38140  onfrALTlem3VD  38145  onfrALTlem2VD  38147  onfrALTVD  38149  relopabVD  38159  ax6e2ndVD  38166  2uasbanhVD  38169  vk15.4jVD  38172  sspwimp  38176  sspwimpVD  38177  sspwimpcf  38178  sspwimpcfVD  38179  suctrALTcf  38180  suctrALTcfVD  38181  suctrALT3  38182  sspwimpALT  38183  unisnALT  38184  ax6e2ndALT  38188  isosctrlem1ALT  38192  iunconlem2  38193  cncfuni  38772  iblcncfioo  38870  stoweidlem14  38907  stoweidlem17  38910  stoweidlem35  38928  stoweidlem57  38950  stirlinglem7  38973  stirlinglem10  38976  fourierdlem54  39053  fourierdlem62  39061  fourierdlem63  39062  fourierdlem65  39064  fourierdlem73  39072  fourierdlem80  39079  fourierdlem82  39081  fourierdlem101  39100  etransclem32  39159  ioorrnopnxr  39203  subsaliuncl  39252  meadjiunlem  39358  ismeannd  39360  voliunsge0lem  39365  volmea  39367  caratheodory  39418  ovnsubaddlem2  39461  hoidmvlelem5  39489  hoiqssbllem2  39513  iinhoiicc  39565  aibandbiaiaiffb  39711  dfdfat2  39860  afvres  39901  tz6.12-afv  39902  ndmaovass  39935  el1fzopredsuc  39948  iccpartiltu  39960  iccelpart  39971  evenprm2  40161  lswn0  40242  ccatpfx  40272  2f1fvneq  40322  fzoopth  40360  nbupgrel  40567  nbusgrvtxm1  40607  nb3gr2nb  40612  cplgruvtxb  40637  pthdivtx  40935  pthdlem2lem  40973  wwlks  41038  wspthnonp  41055  1wlkiswwlks2lem1  41066  wwlksnndef  41111  clwwlksnfi  41220  clwwlksel  41221  clwwlksf1  41224  clwlksf1clwwlklem  41275  umgr3v3e3cycl  41351  frgrncvvdeq  41480  frgr2wwlkeu  41492  frrusgrord0  41503  lincext1  42037