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  582  sylan2br  595  pm2.54  852  orbi2i  912  pm2.31  922  pm2.85  932  pm3.11  994  syl3an1br  1408  syl3an2br  1409  syl3an3br  1410  had1  1604  nic-axALT  1675  speimfw  1964  sbbii  2081  hbsbwOLD  2177  mo4  2566  r19.30  3103  ceqsexv2dOLD  3492  eueq2  3668  ralun  4150  ssunieq  4899  ax6vsep  5248  opelxpi  5661  ordunidif  6367  unizlim  6441  dffo2  6750  dff1o2  6779  resdif  6795  f1o00  6809  fvimacnvALT  7002  fvcofneq  7038  exfo  7050  ressnop0  7098  fsnunfv  7133  2f1fvneq  7206  ovid  7499  ovidig  7500  dfwe2  7719  dford5  7729  onminex  7747  nnsuc  7826  1stnpr  7937  2ndnpr  7938  f1stres  7957  f2ndres  7958  1st2val  7961  2nd2val  7962  frxp  8068  soxp  8071  frxp2  8086  fprlem1  8242  tz7.49  8376  elixpsn  8875  domdifsn  8988  domunsncan  9005  unfi  9095  cnvfi  9100  fineqvlem  9166  unblem4  9195  ordiso2  9420  zfreg  9501  elirrv  9502  inf3lem3  9539  trcl  9637  unir1  9725  ssrankr1  9747  djuunxp  9833  pm54.43lem  9912  infxpenlem  9923  ween  9945  acni3  9957  kmlem1  10061  infdif  10118  ackbij1lem1  10129  fin23lem32  10254  isfin1-3  10296  axdc3lem2  10361  ac6c4  10391  zornn0g  10415  axdclem2  10430  rnct  10435  brdom3  10438  brdom5  10439  brdom4  10440  brdom6disj  10442  konigthlem  10479  pwcfsdom  10494  cfpwsdom  10495  alephom  10496  gruina  10729  grur1  10731  grothomex  10740  grothac  10741  nqpr  10925  axcnre  11075  axpre-sup  11080  ssxr  11202  le2tri3i  11263  muldivdir  11834  0nn0  12416  uzind4  12819  rpnnen1lem5  12894  elfz4  13433  eluzfz  13435  ssfzo12bi  13677  fzoopth  13678  hashgt0elex  14324  hashgt23el  14347  hashxplem  14356  hashfun  14360  ishashinf  14386  wrdsymb1  14476  ccatfv0  14507  lswccats1fst  14559  ccatswrd  14592  ccatpfx  14624  splfv1  14678  repswfsts  14704  cshinj  14734  swrdco  14760  cotr2g  14899  trclun  14937  resqrex  15173  sumeven  16314  ndvdsadd  16337  gcdcllem1  16426  gcdcllem3  16428  lcmftp  16563  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  lcmfun  16572  coprmprod  16588  coprmproddvdslem  16589  divgcdcoprmex  16593  1idssfct  16607  prmodvdslcmf  16975  cshwrepswhash1  17030  xpsfrnel2  17485  xpsff1o  17488  catcone0  17610  initoeu2  17940  clatlem  18425  clatlubcl2  18427  clatglbcl2  18429  chnccat  18549  xpsmnd  18702  xpsgrp  18989  mulgfval  18999  gsmsymgrfix  19357  pmtr3ncom  19404  gsumcom3fi  19908  dprdfeq0  19953  gsumdixp  20254  lspcl  20927  lindfind  21771  lindsind  21772  lindsind2  21774  lindff1  21775  f1linds  21780  evls1maplmhm  22321  mat1dimscm  22419  mdetunilem7  22562  fvmptnn04if  22793  tgcl  22913  elcls  23017  opnnei  23064  neiptopnei  23076  cnpnei  23208  cmpfii  23353  txcnp  23564  xpstps  23754  fbun  23784  isfild  23802  snfil  23808  filconn  23827  isufil2  23852  hauspwpwf1  23931  cnextcn  24011  ustfilxp  24157  ustuqtop4  24188  xpsxms  24478  xpsms  24479  rlmnvc  24647  nmoid  24686  xrsmopn  24757  xrhmeo  24900  cphsqrtcl  25140  iscmet3  25249  iundisj  25505  ioorinv  25533  bddiblnc  25799  dvtaylp  26334  logbid1  26734  logbchbase  26737  relogbcxpb  26753  logbmpt  26754  logbfval  26756  musum  27157  lgsmodeq  27309  lgsmulsqcoprm  27310  2lgs  27374  2sqnn0  27405  pntlem3  27576  ltsval2  27624  noxp1o  27631  conway  27775  cutbdaylt  27794  zsoring  28405  nbupgrel  29418  nbusgrvtxm1  29452  nb3gr2nb  29457  pthdivtx  29800  pthdlem2lem  29840  crctisclwlk  29867  wwlks  29908  wwlksonvtx  29928  wspthnonp  29932  wlkiswwlks2lem1  29942  wwlksnndef  29978  wwlksnfi  29979  clwlkclwwlkf1lem3  30081  clwlkclwwlkf1  30085  clwwlknnn  30108  clwwlkel  30121  clwwlkf1  30124  wwlksext2clwwlk  30132  clwwlknonwwlknonb  30181  umgr3v3e3cycl  30259  frgrncvvdeq  30384  sspval  30798  blo3i  30877  ajfval  30884  spanval  31408  cmcmlem  31666  leopnmid  32213  csmdsymi  32409  chirredlem4  32468  sumdmdlem  32493  iundisjf  32664  padct  32797  iundisjfi  32876  nn0difffzod  32884  hashxpe  32887  fprodex01  32906  xrpxdivcld  33016  gsumfs2d  33144  fldgensdrg  33396  lsmsnorb  33472  mxidlnzr  33548  zringfrac  33635  lactlmhm  33791  extdgval  33810  ccfldextdgrr  33829  ply1annprmidl  33864  pnfneige0  34108  rrhre  34178  esumcocn  34237  hasheuni  34242  sgon  34281  sigapildsys  34319  ddemeas  34393  dya2iocct  34437  dya2iocnrect  34438  eulerpartgbij  34529  eulerpartlemgs2  34537  coinflippv  34641  signstfvneq0  34729  hgt750lemb  34813  bnj1136  35153  bnj1175  35160  bnj1408  35192  fissorduni  35246  fnrelpredd  35247  fineqvnttrclselem1  35277  fineqvnttrclse  35280  unir1regs  35291  onvf1od  35301  vonf1owev  35302  pthhashvtx  35322  spthcycl  35323  upgracycumgr  35347  umgracycusgr  35348  cvmsdisj  35464  mrsubvrs  35716  mppspstlem  35765  problem4  35862  climuzcnv  35865  currybi  35882  dfon2lem7  35981  imageval  36122  filnetlem2  36573  df3nandALT1  36593  lukshef-ax2  36609  arg-ax  36610  weiunpo  36659  regsfromunir1  36670  bj-andnotim  36788  bj-modalbe  36889  bj-hbs1  37013  bj-hbsb2av  37015  bj-2uplex  37223  mptsnunlem  37543  onsucuni3  37572  fvineqsneq  37617  finixpnum  37806  fin2solem  37807  matunitlindflem2  37818  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  poimirlem32  37853  mblfinlem3  37860  itg2addnclem2  37873  itg2addnc  37875  ftc1anclem6  37899  heiborlem3  38014  ismndo2  38075  rngomndo  38136  isfld2  38206  isfldidl  38269  dmncan2  38278  oprabbi  38362  opabbi  38366  ac6s3f  38372  relcnveq3  38520  elrelscnveq3  38800  lsat0cv  39293  pclfinclN  40210  docavalN  41383  djavalN  41395  dochval  41611  djhval  41658  dochexmidlem8  41727  dochkr1  41738  dochkr1OLDN  41739  hdmap1fval  42056  lcmineqlem13  42295  unitscyglem4  42452  fiabv  42791  selvcllem5  42825  mhpind  42837  pellexlem5  43075  rmyabs  43200  jm2.24  43205  islssfgi  43314  pwslnm  43336  dgraaub  43390  omlimcl2  43484  onexoegt  43486  rp-oelim2  43550  oeord2lim  43551  oeord2i  43552  ensucne0OLD  43771  iscard5  43777  clrellem  43863  frege114d  43999  frege55lem1a  44107  frege70  44174  gneispace  44375  ismnushort  44542  3impexpbicom  44721  ee3bir  44744  vk15.4j  44769  onfrALTlem2  44787  ax6e2nd  44799  dfvd1impr  44817  dfvd2impr  44845  e1bir  44871  e2bir  44874  e3bir  44979  suctrALT  45066  19.21a3con13vVD  45092  3impexpbicomVD  45097  tratrbVD  45101  ssralv2VD  45106  truniALTVD  45118  trintALTVD  45120  undif3VD  45122  csbingVD  45124  onfrALTlem3VD  45127  onfrALTlem2VD  45129  onfrALTVD  45131  csbsngVD  45133  csbxpgVD  45134  csbrngVD  45136  csbunigVD  45138  csbfv12gALTVD  45139  relopabVD  45141  ax6e2ndVD  45148  2uasbanhVD  45151  vk15.4jVD  45154  sspwimp  45158  sspwimpVD  45159  sspwimpcf  45160  sspwimpcfVD  45161  suctrALTcf  45162  suctrALTcfVD  45163  suctrALT3  45164  sspwimpALT  45165  unisnALT  45166  ax6e2ndALT  45170  isosctrlem1ALT  45174  iunconnlem2  45175  prclaxpr  45226  wfaxrep  45235  supminfxrrnmpt  45715  limsuppnflem  45954  limsupubuz  45957  cncfuni  46130  iblcncfioo  46222  stoweidlem14  46258  stoweidlem17  46261  stoweidlem35  46279  stoweidlem57  46301  stirlinglem7  46324  stirlinglem10  46327  fourierdlem54  46404  fourierdlem62  46412  fourierdlem63  46413  fourierdlem65  46415  fourierdlem73  46423  fourierdlem80  46430  fourierdlem82  46432  fourierdlem101  46451  etransclem32  46510  ioorrnopnxr  46551  subsaliuncl  46602  meadjiunlem  46709  ismeannd  46711  voliunsge0lem  46716  volmea  46718  caratheodory  46772  ovnsubaddlem2  46815  hoidmvlelem5  46843  hoiqssbllem2  46867  iinhoiicc  46918  aibandbiaiaiffb  47141  funressnvmo  47291  dfdfat2  47374  afvres  47418  tz6.12-afv  47419  ndmaovass  47452  afv2res  47485  tz6.12-afv2  47486  el1fzopredsuc  47571  zp1modne  47592  fundcmpsurinjimaid  47657  iccpartiltu  47668  iccelpart  47679  lswn0  47690  ichnfimlem  47709  prprelb  47762  evenprm2  47960  dfnbgr6  48103  dfsclnbgr6  48104  isgrtri  48189  grlimedgclnbgr  48241  lincext1  48700  resinsnALT  49118  tposideq  49133  sepfsepc  49173  isclatd  49228  intubeu  49229  unilbeu  49230  uprcl2  49434  functhincfun  49694  fullthinc  49695  setc2othin  49711