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  583  sylan2br  596  pm2.54  853  orbi2i  913  pm2.31  923  pm2.85  933  pm3.11  995  syl3an1br  1409  syl3an2br  1410  syl3an3br  1411  had1  1605  nic-axALT  1676  speimfw  1965  sbbii  2082  hbsbwOLD  2178  mo4  2567  r19.30  3105  ceqsexv2dOLD  3481  eueq2  3657  ralun  4139  ssunieq  4887  replem  5223  ax6vsep  5238  opelxpi  5661  ordunidif  6367  unizlim  6441  dffo2  6750  dff1o2  6779  resdif  6795  f1o00  6809  fvimacnvALT  7003  fvcofneq  7039  exfo  7051  ressnop0  7100  fsnunfv  7135  2f1fvneq  7208  ovid  7501  ovidig  7502  dfwe2  7721  dford5  7731  onminex  7749  nnsuc  7828  1stnpr  7939  2ndnpr  7940  f1stres  7959  f2ndres  7960  1st2val  7963  2nd2val  7964  frxp  8069  soxp  8072  frxp2  8087  fprlem1  8243  tz7.49  8377  elixpsn  8878  domdifsn  8991  domunsncan  9008  unfi  9098  cnvfi  9103  fineqvlem  9169  unblem4  9198  ordiso2  9423  zfreg  9504  elirrv  9505  inf3lem3  9542  trcl  9640  unir1  9728  ssrankr1  9750  djuunxp  9836  pm54.43lem  9915  infxpenlem  9926  ween  9948  acni3  9960  kmlem1  10064  infdif  10121  ackbij1lem1  10132  fin23lem32  10257  isfin1-3  10299  axdc3lem2  10364  ac6c4  10394  zornn0g  10418  axdclem2  10433  rnct  10438  brdom3  10441  brdom5  10442  brdom4  10443  brdom6disj  10445  konigthlem  10482  pwcfsdom  10497  cfpwsdom  10498  alephom  10499  gruina  10732  grur1  10734  grothomex  10743  grothac  10744  nqpr  10928  axcnre  11078  axpre-sup  11083  ssxr  11206  le2tri3i  11267  muldivdir  11838  0nn0  12443  uzind4  12847  rpnnen1lem5  12922  elfz4  13462  eluzfz  13464  ssfzo12bi  13707  fzoopth  13708  hashgt0elex  14354  hashgt23el  14377  hashxplem  14386  hashfun  14390  ishashinf  14416  wrdsymb1  14506  ccatfv0  14537  lswccats1fst  14589  ccatswrd  14622  ccatpfx  14654  splfv1  14708  repswfsts  14734  cshinj  14764  swrdco  14790  cotr2g  14929  trclun  14967  resqrex  15203  sumeven  16347  ndvdsadd  16370  gcdcllem1  16459  gcdcllem3  16461  lcmftp  16596  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  lcmfun  16605  coprmprod  16621  coprmproddvdslem  16622  divgcdcoprmex  16626  1idssfct  16640  prmodvdslcmf  17009  cshwrepswhash1  17064  xpsfrnel2  17519  xpsff1o  17522  catcone0  17644  initoeu2  17974  clatlem  18459  clatlubcl2  18461  clatglbcl2  18463  chnccat  18583  xpsmnd  18736  xpsgrp  19026  mulgfval  19036  gsmsymgrfix  19394  pmtr3ncom  19441  gsumcom3fi  19945  dprdfeq0  19990  gsumdixp  20289  lspcl  20962  lindfind  21806  lindsind  21807  lindsind2  21809  lindff1  21810  f1linds  21815  evls1maplmhm  22352  mat1dimscm  22450  mdetunilem7  22593  fvmptnn04if  22824  tgcl  22944  elcls  23048  opnnei  23095  neiptopnei  23107  cnpnei  23239  cmpfii  23384  txcnp  23595  xpstps  23785  fbun  23815  isfild  23833  snfil  23839  filconn  23858  isufil2  23883  hauspwpwf1  23962  cnextcn  24042  ustfilxp  24188  ustuqtop4  24219  xpsxms  24509  xpsms  24510  rlmnvc  24678  nmoid  24717  xrsmopn  24788  xrhmeo  24923  cphsqrtcl  25161  iscmet3  25270  iundisj  25525  ioorinv  25553  bddiblnc  25819  dvtaylp  26347  logbid1  26745  logbchbase  26748  relogbcxpb  26764  logbmpt  26765  logbfval  26767  musum  27168  lgsmodeq  27319  lgsmulsqcoprm  27320  2lgs  27384  2sqnn0  27415  pntlem3  27586  ltsval2  27634  noxp1o  27641  conway  27785  cutbdaylt  27804  zsoring  28415  nbupgrel  29428  nbusgrvtxm1  29462  nb3gr2nb  29467  pthdivtx  29810  pthdlem2lem  29850  crctisclwlk  29877  wwlks  29918  wwlksonvtx  29938  wspthnonp  29942  wlkiswwlks2lem1  29952  wwlksnndef  29988  wwlksnfi  29989  clwlkclwwlkf1lem3  30091  clwlkclwwlkf1  30095  clwwlknnn  30118  clwwlkel  30131  clwwlkf1  30134  wwlksext2clwwlk  30142  clwwlknonwwlknonb  30191  umgr3v3e3cycl  30269  frgrncvvdeq  30394  sspval  30809  blo3i  30888  ajfval  30895  spanval  31419  cmcmlem  31677  leopnmid  32224  csmdsymi  32420  chirredlem4  32479  sumdmdlem  32504  iundisjf  32674  iundisjfi  32884  nn0difffzod  32892  hashxpe  32895  fprodex01  32913  xrpxdivcld  33009  gsumfs2d  33137  fldgensdrg  33390  lsmsnorb  33466  mxidlnzr  33542  zringfrac  33629  lactlmhm  33794  extdgval  33813  ccfldextdgrr  33832  ply1annprmidl  33867  pnfneige0  34111  rrhre  34181  esumcocn  34240  hasheuni  34245  sgon  34284  sigapildsys  34322  ddemeas  34396  dya2iocct  34440  dya2iocnrect  34441  eulerpartgbij  34532  eulerpartlemgs2  34540  coinflippv  34644  signstfvneq0  34732  hgt750lemb  34816  bnj1136  35155  bnj1175  35162  bnj1408  35194  fissorduni  35249  fnrelpredd  35250  fineqvnttrclselem1  35281  fineqvnttrclse  35284  unir1regs  35295  onvf1od  35305  vonf1owev  35306  pthhashvtx  35326  spthcycl  35327  upgracycumgr  35351  umgracycusgr  35352  cvmsdisj  35468  mrsubvrs  35720  mppspstlem  35769  problem4  35866  climuzcnv  35869  currybi  35886  dfon2lem7  35985  imageval  36126  filnetlem2  36577  df3nandALT1  36597  lukshef-ax2  36613  arg-ax  36614  weiunpo  36663  axtco  36669  dfttc4lem2  36727  regsfromunir1  36738  bj-andnotim  36869  bj-modalbe  37001  bj-hbs1  37135  bj-hbsb2av  37137  bj-2uplex  37345  bj-axseprep  37397  mptsnunlem  37668  onsucuni3  37697  fvineqsneq  37742  finixpnum  37940  fin2solem  37941  matunitlindflem2  37952  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  poimirlem32  37987  mblfinlem3  37994  itg2addnclem2  38007  itg2addnc  38009  ftc1anclem6  38033  heiborlem3  38148  ismndo2  38209  rngomndo  38270  isfld2  38340  isfldidl  38403  dmncan2  38412  oprabbi  38496  opabbi  38500  ac6s3f  38506  relcnveq3  38662  elrelscnveq3  38962  lsat0cv  39493  pclfinclN  40410  docavalN  41583  djavalN  41595  dochval  41811  djhval  41858  dochexmidlem8  41927  dochkr1  41938  dochkr1OLDN  41939  hdmap1fval  42256  lcmineqlem13  42494  unitscyglem4  42651  fiabv  42995  selvcllem5  43029  mhpind  43041  pellexlem5  43279  rmyabs  43404  jm2.24  43409  islssfgi  43518  pwslnm  43540  dgraaub  43594  omlimcl2  43688  onexoegt  43690  rp-oelim2  43754  oeord2lim  43755  oeord2i  43756  ensucne0OLD  43975  iscard5  43981  clrellem  44067  frege114d  44203  frege55lem1a  44311  frege70  44378  gneispace  44579  ismnushort  44746  3impexpbicom  44925  ee3bir  44948  vk15.4j  44973  onfrALTlem2  44991  ax6e2nd  45003  dfvd1impr  45021  dfvd2impr  45049  e1bir  45075  e2bir  45078  e3bir  45183  suctrALT  45270  19.21a3con13vVD  45296  3impexpbicomVD  45301  tratrbVD  45305  ssralv2VD  45310  truniALTVD  45322  trintALTVD  45324  undif3VD  45326  csbingVD  45328  onfrALTlem3VD  45331  onfrALTlem2VD  45333  onfrALTVD  45335  csbsngVD  45337  csbxpgVD  45338  csbrngVD  45340  csbunigVD  45342  csbfv12gALTVD  45343  relopabVD  45345  ax6e2ndVD  45352  2uasbanhVD  45355  vk15.4jVD  45358  sspwimp  45362  sspwimpVD  45363  sspwimpcf  45364  sspwimpcfVD  45365  suctrALTcf  45366  suctrALTcfVD  45367  suctrALT3  45368  sspwimpALT  45369  unisnALT  45370  ax6e2ndALT  45374  isosctrlem1ALT  45378  iunconnlem2  45379  prclaxpr  45430  wfaxrep  45439  supminfxrrnmpt  45917  limsuppnflem  46156  limsupubuz  46159  cncfuni  46332  iblcncfioo  46424  stoweidlem14  46460  stoweidlem17  46463  stoweidlem35  46481  stoweidlem57  46503  stirlinglem7  46526  stirlinglem10  46529  fourierdlem54  46606  fourierdlem62  46614  fourierdlem63  46615  fourierdlem65  46617  fourierdlem73  46625  fourierdlem80  46632  fourierdlem82  46634  fourierdlem101  46653  etransclem32  46712  ioorrnopnxr  46753  subsaliuncl  46804  meadjiunlem  46911  ismeannd  46913  voliunsge0lem  46918  volmea  46920  caratheodory  46974  ovnsubaddlem2  47017  hoidmvlelem5  47045  hoiqssbllem2  47069  iinhoiicc  47120  aibandbiaiaiffb  47355  funressnvmo  47505  dfdfat2  47588  afvres  47632  tz6.12-afv  47633  ndmaovass  47666  afv2res  47699  tz6.12-afv2  47700  el1fzopredsuc  47786  zp1modne  47812  fundcmpsurinjimaid  47883  iccpartiltu  47894  iccelpart  47905  lswn0  47916  ichnfimlem  47935  prprelb  47988  indprmfz  48105  evenprm2  48202  dfnbgr6  48345  dfsclnbgr6  48346  isgrtri  48431  grlimedgclnbgr  48483  lincext1  48942  resinsnALT  49360  tposideq  49375  sepfsepc  49415  isclatd  49470  intubeu  49471  unilbeu  49472  uprcl2  49676  functhincfun  49936  fullthinc  49937  setc2othin  49953