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  5659  ordunidif  6365  unizlim  6439  dffo2  6748  dff1o2  6777  resdif  6793  f1o00  6807  fvimacnvALT  7001  fvcofneq  7037  exfo  7049  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  8067  soxp  8070  frxp2  8085  fprlem1  8241  tz7.49  8375  elixpsn  8876  domdifsn  8989  domunsncan  9006  unfi  9096  cnvfi  9101  fineqvlem  9167  unblem4  9196  ordiso2  9421  zfreg  9502  elirrv  9503  inf3lem3  9540  trcl  9638  unir1  9726  ssrankr1  9748  djuunxp  9834  pm54.43lem  9913  infxpenlem  9924  ween  9946  acni3  9958  kmlem1  10062  infdif  10119  ackbij1lem1  10130  fin23lem32  10255  isfin1-3  10297  axdc3lem2  10362  ac6c4  10392  zornn0g  10416  axdclem2  10431  rnct  10436  brdom3  10439  brdom5  10440  brdom4  10441  brdom6disj  10443  konigthlem  10480  pwcfsdom  10495  cfpwsdom  10496  alephom  10497  gruina  10730  grur1  10732  grothomex  10741  grothac  10742  nqpr  10926  axcnre  11076  axpre-sup  11081  ssxr  11204  le2tri3i  11265  muldivdir  11836  0nn0  12441  uzind4  12845  rpnnen1lem5  12920  elfz4  13460  eluzfz  13462  ssfzo12bi  13705  fzoopth  13706  hashgt0elex  14352  hashgt23el  14375  hashxplem  14384  hashfun  14388  ishashinf  14414  wrdsymb1  14504  ccatfv0  14535  lswccats1fst  14587  ccatswrd  14620  ccatpfx  14652  splfv1  14706  repswfsts  14732  cshinj  14762  swrdco  14788  cotr2g  14927  trclun  14965  resqrex  15201  sumeven  16345  ndvdsadd  16368  gcdcllem1  16457  gcdcllem3  16459  lcmftp  16594  lcmfunsnlem2lem2  16597  lcmfunsnlem2  16598  lcmfun  16603  coprmprod  16619  coprmproddvdslem  16620  divgcdcoprmex  16624  1idssfct  16638  prmodvdslcmf  17007  cshwrepswhash1  17062  xpsfrnel2  17517  xpsff1o  17520  catcone0  17642  initoeu2  17972  clatlem  18457  clatlubcl2  18459  clatglbcl2  18461  chnccat  18581  xpsmnd  18734  xpsgrp  19024  mulgfval  19034  gsmsymgrfix  19392  pmtr3ncom  19439  gsumcom3fi  19943  dprdfeq0  19988  gsumdixp  20287  lspcl  20960  lindfind  21804  lindsind  21805  lindsind2  21807  lindff1  21808  f1linds  21813  evls1maplmhm  22351  mat1dimscm  22449  mdetunilem7  22592  fvmptnn04if  22823  tgcl  22943  elcls  23047  opnnei  23094  neiptopnei  23106  cnpnei  23238  cmpfii  23383  txcnp  23594  xpstps  23784  fbun  23814  isfild  23832  snfil  23838  filconn  23857  isufil2  23882  hauspwpwf1  23961  cnextcn  24041  ustfilxp  24187  ustuqtop4  24218  xpsxms  24508  xpsms  24509  rlmnvc  24677  nmoid  24716  xrsmopn  24787  xrhmeo  24922  cphsqrtcl  25160  iscmet3  25269  iundisj  25524  ioorinv  25552  bddiblnc  25818  dvtaylp  26349  logbid1  26749  logbchbase  26752  relogbcxpb  26768  logbmpt  26769  logbfval  26771  musum  27172  lgsmodeq  27324  lgsmulsqcoprm  27325  2lgs  27389  2sqnn0  27420  pntlem3  27591  ltsval2  27639  noxp1o  27646  conway  27790  cutbdaylt  27809  zsoring  28420  nbupgrel  29433  nbusgrvtxm1  29467  nb3gr2nb  29472  pthdivtx  29815  pthdlem2lem  29855  crctisclwlk  29882  wwlks  29923  wwlksonvtx  29943  wspthnonp  29947  wlkiswwlks2lem1  29957  wwlksnndef  29993  wwlksnfi  29994  clwlkclwwlkf1lem3  30096  clwlkclwwlkf1  30100  clwwlknnn  30123  clwwlkel  30136  clwwlkf1  30139  wwlksext2clwwlk  30147  clwwlknonwwlknonb  30196  umgr3v3e3cycl  30274  frgrncvvdeq  30399  sspval  30814  blo3i  30893  ajfval  30900  spanval  31424  cmcmlem  31682  leopnmid  32229  csmdsymi  32425  chirredlem4  32484  sumdmdlem  32509  iundisjf  32679  iundisjfi  32889  nn0difffzod  32897  hashxpe  32900  fprodex01  32918  xrpxdivcld  33014  gsumfs2d  33142  fldgensdrg  33395  lsmsnorb  33471  mxidlnzr  33547  zringfrac  33634  lactlmhm  33799  extdgval  33818  ccfldextdgrr  33837  ply1annprmidl  33872  pnfneige0  34116  rrhre  34186  esumcocn  34245  hasheuni  34250  sgon  34289  sigapildsys  34327  ddemeas  34401  dya2iocct  34445  dya2iocnrect  34446  eulerpartgbij  34537  eulerpartlemgs2  34545  coinflippv  34649  signstfvneq0  34737  hgt750lemb  34821  bnj1136  35160  bnj1175  35167  bnj1408  35199  fissorduni  35254  fnrelpredd  35255  fineqvnttrclselem1  35286  fineqvnttrclse  35289  unir1regs  35300  onvf1od  35310  vonf1owev  35311  pthhashvtx  35331  spthcycl  35332  upgracycumgr  35356  umgracycusgr  35357  cvmsdisj  35473  mrsubvrs  35725  mppspstlem  35774  problem4  35871  climuzcnv  35874  currybi  35891  dfon2lem7  35990  imageval  36131  filnetlem2  36582  df3nandALT1  36602  lukshef-ax2  36618  arg-ax  36619  weiunpo  36668  axtco  36674  dfttc4lem2  36732  regsfromunir1  36743  bj-andnotim  36866  bj-modalbe  36998  bj-hbs1  37132  bj-hbsb2av  37134  bj-2uplex  37342  bj-axseprep  37394  mptsnunlem  37665  onsucuni3  37694  fvineqsneq  37739  finixpnum  37937  fin2solem  37938  matunitlindflem2  37949  poimirlem6  37958  poimirlem7  37959  poimirlem8  37960  poimirlem18  37970  poimirlem21  37973  poimirlem22  37974  poimirlem32  37984  mblfinlem3  37991  itg2addnclem2  38004  itg2addnc  38006  ftc1anclem6  38030  heiborlem3  38145  ismndo2  38206  rngomndo  38267  isfld2  38337  isfldidl  38400  dmncan2  38409  oprabbi  38493  opabbi  38497  ac6s3f  38503  relcnveq3  38659  elrelscnveq3  38959  lsat0cv  39490  pclfinclN  40407  docavalN  41580  djavalN  41592  dochval  41808  djhval  41855  dochexmidlem8  41924  dochkr1  41935  dochkr1OLDN  41936  hdmap1fval  42253  lcmineqlem13  42491  unitscyglem4  42648  fiabv  42992  selvcllem5  43026  mhpind  43038  pellexlem5  43276  rmyabs  43401  jm2.24  43406  islssfgi  43515  pwslnm  43537  dgraaub  43591  omlimcl2  43685  onexoegt  43687  rp-oelim2  43751  oeord2lim  43752  oeord2i  43753  ensucne0OLD  43972  iscard5  43978  clrellem  44064  frege114d  44200  frege55lem1a  44308  frege70  44375  gneispace  44576  ismnushort  44743  3impexpbicom  44922  ee3bir  44945  vk15.4j  44970  onfrALTlem2  44988  ax6e2nd  45000  dfvd1impr  45018  dfvd2impr  45046  e1bir  45072  e2bir  45075  e3bir  45180  suctrALT  45267  19.21a3con13vVD  45293  3impexpbicomVD  45298  tratrbVD  45302  ssralv2VD  45307  truniALTVD  45319  trintALTVD  45321  undif3VD  45323  csbingVD  45325  onfrALTlem3VD  45328  onfrALTlem2VD  45330  onfrALTVD  45332  csbsngVD  45334  csbxpgVD  45335  csbrngVD  45337  csbunigVD  45339  csbfv12gALTVD  45340  relopabVD  45342  ax6e2ndVD  45349  2uasbanhVD  45352  vk15.4jVD  45355  sspwimp  45359  sspwimpVD  45360  sspwimpcf  45361  sspwimpcfVD  45362  suctrALTcf  45363  suctrALTcfVD  45364  suctrALT3  45365  sspwimpALT  45366  unisnALT  45367  ax6e2ndALT  45371  isosctrlem1ALT  45375  iunconnlem2  45376  prclaxpr  45427  wfaxrep  45436  supminfxrrnmpt  45914  limsuppnflem  46153  limsupubuz  46156  cncfuni  46329  iblcncfioo  46421  stoweidlem14  46457  stoweidlem17  46460  stoweidlem35  46478  stoweidlem57  46500  stirlinglem7  46523  stirlinglem10  46526  fourierdlem54  46603  fourierdlem62  46611  fourierdlem63  46612  fourierdlem65  46614  fourierdlem73  46622  fourierdlem80  46629  fourierdlem82  46631  fourierdlem101  46650  etransclem32  46709  ioorrnopnxr  46750  subsaliuncl  46801  meadjiunlem  46908  ismeannd  46910  voliunsge0lem  46915  volmea  46917  caratheodory  46971  ovnsubaddlem2  47014  hoidmvlelem5  47042  hoiqssbllem2  47066  iinhoiicc  47117  aibandbiaiaiffb  47340  funressnvmo  47490  dfdfat2  47573  afvres  47617  tz6.12-afv  47618  ndmaovass  47651  afv2res  47684  tz6.12-afv2  47685  el1fzopredsuc  47771  zp1modne  47797  fundcmpsurinjimaid  47868  iccpartiltu  47879  iccelpart  47890  lswn0  47901  ichnfimlem  47920  prprelb  47973  indprmfz  48090  evenprm2  48187  dfnbgr6  48330  dfsclnbgr6  48331  isgrtri  48416  grlimedgclnbgr  48468  lincext1  48927  resinsnALT  49345  tposideq  49360  sepfsepc  49400  isclatd  49455  intubeu  49456  unilbeu  49457  uprcl2  49661  functhincfun  49921  fullthinc  49922  setc2othin  49938