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  3494  eueq2  3670  ralun  4152  ssunieq  4901  ax6vsep  5250  opelxpi  5669  ordunidif  6375  unizlim  6449  dffo2  6758  dff1o2  6787  resdif  6803  f1o00  6817  fvimacnvALT  7011  fvcofneq  7047  exfo  7059  ressnop0  7108  fsnunfv  7143  2f1fvneq  7216  ovid  7509  ovidig  7510  dfwe2  7729  dford5  7739  onminex  7757  nnsuc  7836  1stnpr  7947  2ndnpr  7948  f1stres  7967  f2ndres  7968  1st2val  7971  2nd2val  7972  frxp  8078  soxp  8081  frxp2  8096  fprlem1  8252  tz7.49  8386  elixpsn  8887  domdifsn  9000  domunsncan  9017  unfi  9107  cnvfi  9112  fineqvlem  9178  unblem4  9207  ordiso2  9432  zfreg  9513  elirrv  9514  inf3lem3  9551  trcl  9649  unir1  9737  ssrankr1  9759  djuunxp  9845  pm54.43lem  9924  infxpenlem  9935  ween  9957  acni3  9969  kmlem1  10073  infdif  10130  ackbij1lem1  10141  fin23lem32  10266  isfin1-3  10308  axdc3lem2  10373  ac6c4  10403  zornn0g  10427  axdclem2  10442  rnct  10447  brdom3  10450  brdom5  10451  brdom4  10452  brdom6disj  10454  konigthlem  10491  pwcfsdom  10506  cfpwsdom  10507  alephom  10508  gruina  10741  grur1  10743  grothomex  10752  grothac  10753  nqpr  10937  axcnre  11087  axpre-sup  11092  ssxr  11214  le2tri3i  11275  muldivdir  11846  0nn0  12428  uzind4  12831  rpnnen1lem5  12906  elfz4  13445  eluzfz  13447  ssfzo12bi  13689  fzoopth  13690  hashgt0elex  14336  hashgt23el  14359  hashxplem  14368  hashfun  14372  ishashinf  14398  wrdsymb1  14488  ccatfv0  14519  lswccats1fst  14571  ccatswrd  14604  ccatpfx  14636  splfv1  14690  repswfsts  14716  cshinj  14746  swrdco  14772  cotr2g  14911  trclun  14949  resqrex  15185  sumeven  16326  ndvdsadd  16349  gcdcllem1  16438  gcdcllem3  16440  lcmftp  16575  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  lcmfun  16584  coprmprod  16600  coprmproddvdslem  16601  divgcdcoprmex  16605  1idssfct  16619  prmodvdslcmf  16987  cshwrepswhash1  17042  xpsfrnel2  17497  xpsff1o  17500  catcone0  17622  initoeu2  17952  clatlem  18437  clatlubcl2  18439  clatglbcl2  18441  chnccat  18561  xpsmnd  18714  xpsgrp  19001  mulgfval  19011  gsmsymgrfix  19369  pmtr3ncom  19416  gsumcom3fi  19920  dprdfeq0  19965  gsumdixp  20266  lspcl  20939  lindfind  21783  lindsind  21784  lindsind2  21786  lindff1  21787  f1linds  21792  evls1maplmhm  22333  mat1dimscm  22431  mdetunilem7  22574  fvmptnn04if  22805  tgcl  22925  elcls  23029  opnnei  23076  neiptopnei  23088  cnpnei  23220  cmpfii  23365  txcnp  23576  xpstps  23766  fbun  23796  isfild  23814  snfil  23820  filconn  23839  isufil2  23864  hauspwpwf1  23943  cnextcn  24023  ustfilxp  24169  ustuqtop4  24200  xpsxms  24490  xpsms  24491  rlmnvc  24659  nmoid  24698  xrsmopn  24769  xrhmeo  24912  cphsqrtcl  25152  iscmet3  25261  iundisj  25517  ioorinv  25545  bddiblnc  25811  dvtaylp  26346  logbid1  26746  logbchbase  26749  relogbcxpb  26765  logbmpt  26766  logbfval  26768  musum  27169  lgsmodeq  27321  lgsmulsqcoprm  27322  2lgs  27386  2sqnn0  27417  pntlem3  27588  ltsval2  27636  noxp1o  27643  conway  27787  cutbdaylt  27806  zsoring  28417  nbupgrel  29430  nbusgrvtxm1  29464  nb3gr2nb  29469  pthdivtx  29812  pthdlem2lem  29852  crctisclwlk  29879  wwlks  29920  wwlksonvtx  29940  wspthnonp  29944  wlkiswwlks2lem1  29954  wwlksnndef  29990  wwlksnfi  29991  clwlkclwwlkf1lem3  30093  clwlkclwwlkf1  30097  clwwlknnn  30120  clwwlkel  30133  clwwlkf1  30136  wwlksext2clwwlk  30144  clwwlknonwwlknonb  30193  umgr3v3e3cycl  30271  frgrncvvdeq  30396  sspval  30811  blo3i  30890  ajfval  30897  spanval  31421  cmcmlem  31679  leopnmid  32226  csmdsymi  32422  chirredlem4  32481  sumdmdlem  32506  iundisjf  32676  padct  32808  iundisjfi  32887  nn0difffzod  32895  hashxpe  32898  fprodex01  32917  xrpxdivcld  33027  gsumfs2d  33155  fldgensdrg  33408  lsmsnorb  33484  mxidlnzr  33560  zringfrac  33647  lactlmhm  33812  extdgval  33831  ccfldextdgrr  33850  ply1annprmidl  33885  pnfneige0  34129  rrhre  34199  esumcocn  34258  hasheuni  34263  sgon  34302  sigapildsys  34340  ddemeas  34414  dya2iocct  34458  dya2iocnrect  34459  eulerpartgbij  34550  eulerpartlemgs2  34558  coinflippv  34662  signstfvneq0  34750  hgt750lemb  34834  bnj1136  35173  bnj1175  35180  bnj1408  35212  fissorduni  35267  fnrelpredd  35268  fineqvnttrclselem1  35299  fineqvnttrclse  35302  unir1regs  35313  onvf1od  35323  vonf1owev  35324  pthhashvtx  35344  spthcycl  35345  upgracycumgr  35369  umgracycusgr  35370  cvmsdisj  35486  mrsubvrs  35738  mppspstlem  35787  problem4  35884  climuzcnv  35887  currybi  35904  dfon2lem7  36003  imageval  36144  filnetlem2  36595  df3nandALT1  36615  lukshef-ax2  36631  arg-ax  36632  weiunpo  36681  regsfromunir1  36692  bj-andnotim  36813  bj-modalbe  36933  bj-hbs1  37060  bj-hbsb2av  37062  bj-2uplex  37270  bj-axseprep  37322  mptsnunlem  37593  onsucuni3  37622  fvineqsneq  37667  finixpnum  37856  fin2solem  37857  matunitlindflem2  37868  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem18  37889  poimirlem21  37892  poimirlem22  37893  poimirlem32  37903  mblfinlem3  37910  itg2addnclem2  37923  itg2addnc  37925  ftc1anclem6  37949  heiborlem3  38064  ismndo2  38125  rngomndo  38186  isfld2  38256  isfldidl  38319  dmncan2  38328  oprabbi  38412  opabbi  38416  ac6s3f  38422  relcnveq3  38578  elrelscnveq3  38878  lsat0cv  39409  pclfinclN  40326  docavalN  41499  djavalN  41511  dochval  41727  djhval  41774  dochexmidlem8  41843  dochkr1  41854  dochkr1OLDN  41855  hdmap1fval  42172  lcmineqlem13  42411  unitscyglem4  42568  fiabv  42906  selvcllem5  42940  mhpind  42952  pellexlem5  43190  rmyabs  43315  jm2.24  43320  islssfgi  43429  pwslnm  43451  dgraaub  43505  omlimcl2  43599  onexoegt  43601  rp-oelim2  43665  oeord2lim  43666  oeord2i  43667  ensucne0OLD  43886  iscard5  43892  clrellem  43978  frege114d  44114  frege55lem1a  44222  frege70  44289  gneispace  44490  ismnushort  44657  3impexpbicom  44836  ee3bir  44859  vk15.4j  44884  onfrALTlem2  44902  ax6e2nd  44914  dfvd1impr  44932  dfvd2impr  44960  e1bir  44986  e2bir  44989  e3bir  45094  suctrALT  45181  19.21a3con13vVD  45207  3impexpbicomVD  45212  tratrbVD  45216  ssralv2VD  45221  truniALTVD  45233  trintALTVD  45235  undif3VD  45237  csbingVD  45239  onfrALTlem3VD  45242  onfrALTlem2VD  45244  onfrALTVD  45246  csbsngVD  45248  csbxpgVD  45249  csbrngVD  45251  csbunigVD  45253  csbfv12gALTVD  45254  relopabVD  45256  ax6e2ndVD  45263  2uasbanhVD  45266  vk15.4jVD  45269  sspwimp  45273  sspwimpVD  45274  sspwimpcf  45275  sspwimpcfVD  45276  suctrALTcf  45277  suctrALTcfVD  45278  suctrALT3  45279  sspwimpALT  45280  unisnALT  45281  ax6e2ndALT  45285  isosctrlem1ALT  45289  iunconnlem2  45290  prclaxpr  45341  wfaxrep  45350  supminfxrrnmpt  45829  limsuppnflem  46068  limsupubuz  46071  cncfuni  46244  iblcncfioo  46336  stoweidlem14  46372  stoweidlem17  46375  stoweidlem35  46393  stoweidlem57  46415  stirlinglem7  46438  stirlinglem10  46441  fourierdlem54  46518  fourierdlem62  46526  fourierdlem63  46527  fourierdlem65  46529  fourierdlem73  46537  fourierdlem80  46544  fourierdlem82  46546  fourierdlem101  46565  etransclem32  46624  ioorrnopnxr  46665  subsaliuncl  46716  meadjiunlem  46823  ismeannd  46825  voliunsge0lem  46830  volmea  46832  caratheodory  46886  ovnsubaddlem2  46929  hoidmvlelem5  46957  hoiqssbllem2  46981  iinhoiicc  47032  aibandbiaiaiffb  47255  funressnvmo  47405  dfdfat2  47488  afvres  47532  tz6.12-afv  47533  ndmaovass  47566  afv2res  47599  tz6.12-afv2  47600  el1fzopredsuc  47685  zp1modne  47706  fundcmpsurinjimaid  47771  iccpartiltu  47782  iccelpart  47793  lswn0  47804  ichnfimlem  47823  prprelb  47876  evenprm2  48074  dfnbgr6  48217  dfsclnbgr6  48218  isgrtri  48303  grlimedgclnbgr  48355  lincext1  48814  resinsnALT  49232  tposideq  49247  sepfsepc  49287  isclatd  49342  intubeu  49343  unilbeu  49344  uprcl2  49548  functhincfun  49808  fullthinc  49809  setc2othin  49825