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  853  orbi2i  913  pm2.31  923  pm2.85  933  pm3.11  995  syl3an1br  1408  syl3an2br  1409  syl3an3br  1410  had1  1603  nic-axALT  1674  speimfw  1963  sbbii  2076  hbsbwOLD  2172  mobii  2548  mo4  2566  r19.30  3120  r19.30OLD  3121  ceqsexv2dOLD  3534  eueq2  3716  ralun  4198  ssunieq  4943  ax6vsep  5303  opelxpi  5722  ordunidif  6433  unizlim  6507  dffo2  6824  dff1o2  6853  resdif  6869  f1o00  6883  fvimacnvALT  7077  fvcofneq  7113  exfo  7125  ressnop0  7173  fsnunfv  7207  ovid  7574  ovidig  7575  dfwe2  7794  dford5  7804  onminex  7822  nnsuc  7905  1stnpr  8018  2ndnpr  8019  f1stres  8038  f2ndres  8039  1st2val  8042  2nd2val  8043  frxp  8151  soxp  8154  frxp2  8169  fprlem1  8325  tz7.49  8485  elixpsn  8977  domdifsn  9094  domunsncan  9112  unfi  9211  cnvfi  9216  fineqvlem  9298  unblem4  9331  ordiso2  9555  zfreg  9635  inf3lem3  9670  trcl  9768  unir1  9853  ssrankr1  9875  djuunxp  9961  pm54.43lem  10040  infxpenlem  10053  ween  10075  acni3  10087  kmlem1  10191  infdif  10248  ackbij1lem1  10259  fin23lem32  10384  isfin1-3  10426  axdc3lem2  10491  ac6c4  10521  zornn0g  10545  axdclem2  10560  rnct  10565  brdom3  10568  brdom5  10569  brdom4  10570  brdom6disj  10572  konigthlem  10608  pwcfsdom  10623  cfpwsdom  10624  alephom  10625  gruina  10858  grur1  10860  grothomex  10869  grothac  10870  nqpr  11054  axcnre  11204  axpre-sup  11209  ssxr  11330  le2tri3i  11391  muldivdir  11960  0nn0  12541  uzind4  12948  rpnnen1lem5  13023  elfz4  13557  eluzfz  13559  ssfzo12bi  13800  fzoopth  13801  hashgt0elex  14440  hashgt23el  14463  hashxplem  14472  hashfun  14476  ishashinf  14502  wrdsymb1  14591  ccatfv0  14621  lswccats1fst  14673  ccatswrd  14706  ccatpfx  14739  splfv1  14793  repswfsts  14819  cshinj  14849  swrdco  14876  cotr2g  15015  trclun  15053  resqrex  15289  sumeven  16424  ndvdsadd  16447  gcdcllem1  16536  gcdcllem3  16538  lcmftp  16673  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfun  16682  coprmprod  16698  coprmproddvdslem  16699  divgcdcoprmex  16703  1idssfct  16717  prmodvdslcmf  17085  cshwrepswhash1  17140  xpsfrnel2  17609  xpsff1o  17612  catcone0  17730  initoeu2  18061  clatlem  18547  clatlubcl2  18549  clatglbcl2  18551  xpsmnd  18790  xpsgrp  19077  mulgfval  19087  gsmsymgrfix  19446  pmtr3ncom  19493  gsumcom3fi  19997  dprdfeq0  20042  gsumdixp  20316  lspcl  20974  lindfind  21836  lindsind  21837  lindsind2  21839  lindff1  21840  f1linds  21845  evls1maplmhm  22381  mat1dimscm  22481  mdetunilem7  22624  fvmptnn04if  22855  tgcl  22976  elcls  23081  opnnei  23128  neiptopnei  23140  cnpnei  23272  cmpfii  23417  txcnp  23628  xpstps  23818  fbun  23848  isfild  23866  snfil  23872  filconn  23891  isufil2  23916  hauspwpwf1  23995  cnextcn  24075  ustfilxp  24221  ustuqtop4  24253  xpsxms  24547  xpsms  24548  rlmnvc  24724  nmoid  24763  xrsmopn  24834  xrhmeo  24977  cphsqrtcl  25218  iscmet3  25327  iundisj  25583  ioorinv  25611  bddiblnc  25877  dvtaylp  26412  logbid1  26811  logbchbase  26814  relogbcxpb  26830  logbmpt  26831  logbfval  26833  musum  27234  lgsmodeq  27386  lgsmulsqcoprm  27387  2lgs  27451  2sqnn0  27482  pntlem3  27653  sltval2  27701  noxp1o  27708  conway  27844  scutbdaylt  27863  nbupgrel  29362  nbusgrvtxm1  29396  nb3gr2nb  29401  pthdivtx  29747  pthdlem2lem  29787  crctisclwlk  29814  wwlks  29855  wwlksonvtx  29875  wspthnonp  29879  wlkiswwlks2lem1  29889  wwlksnndef  29925  wwlksnfi  29926  clwlkclwwlkf1lem3  30025  clwlkclwwlkf1  30029  clwwlknnn  30052  clwwlkel  30065  clwwlkf1  30068  wwlksext2clwwlk  30076  clwwlknonwwlknonb  30125  umgr3v3e3cycl  30203  frgrncvvdeq  30328  sspval  30742  blo3i  30821  ajfval  30828  spanval  31352  cmcmlem  31610  leopnmid  32157  csmdsymi  32353  chirredlem4  32412  sumdmdlem  32437  iundisjf  32602  padct  32731  iundisjfi  32798  nn0difffzod  32808  hashxpe  32811  fprodex01  32827  xrpxdivcld  32917  gsumfs2d  33058  fldgensdrg  33316  lsmsnorb  33419  mxidlnzr  33495  zringfrac  33582  lactlmhm  33685  extdgval  33705  ccfldextdgrr  33722  ply1annprmidl  33750  pnfneige0  33950  rrhre  34022  esumcocn  34081  hasheuni  34086  sgon  34125  sigapildsys  34163  ddemeas  34237  dya2iocct  34282  dya2iocnrect  34283  eulerpartgbij  34374  eulerpartlemgs2  34382  coinflippv  34486  signstfvneq0  34587  hgt750lemb  34671  bnj1136  35011  bnj1175  35018  bnj1408  35050  fnrelpredd  35103  pthhashvtx  35133  spthcycl  35134  upgracycumgr  35158  umgracycusgr  35159  cvmsdisj  35275  mrsubvrs  35527  mppspstlem  35576  problem4  35673  climuzcnv  35676  currybi  35693  dfon2lem7  35790  imageval  35931  filnetlem2  36380  df3nandALT1  36400  lukshef-ax2  36416  arg-ax  36417  weiunpo  36466  bj-andnotim  36589  bj-modalbe  36689  bj-hbs1  36813  bj-hbsb2av  36815  bj-2uplex  37023  mptsnunlem  37339  onsucuni3  37368  fvineqsneq  37413  finixpnum  37612  fin2solem  37613  matunitlindflem2  37624  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem32  37659  mblfinlem3  37666  itg2addnclem2  37679  itg2addnc  37681  ftc1anclem6  37705  heiborlem3  37820  ismndo2  37881  rngomndo  37942  isfld2  38012  isfldidl  38075  dmncan2  38084  oprabbi  38168  opabbi  38172  ac6s3f  38178  relcnveq3  38322  elrelscnveq3  38492  lsat0cv  39034  pclfinclN  39952  docavalN  41125  djavalN  41137  dochval  41353  djhval  41400  dochexmidlem8  41469  dochkr1  41480  dochkr1OLDN  41481  hdmap1fval  41798  lcmineqlem13  42042  unitscyglem4  42199  fiabv  42546  selvcllem5  42592  mhpind  42604  pellexlem5  42844  rmyabs  42970  jm2.24  42975  islssfgi  43084  pwslnm  43106  dgraaub  43160  omlimcl2  43254  onexoegt  43256  rp-oelim2  43321  oeord2lim  43322  oeord2i  43323  ensucne0OLD  43543  iscard5  43549  clrellem  43635  frege114d  43771  frege55lem1a  43879  frege70  43946  gneispace  44147  ismnushort  44320  3impexpbicom  44500  ee3bir  44523  vk15.4j  44548  onfrALTlem2  44566  ax6e2nd  44578  dfvd1impr  44596  dfvd2impr  44624  e1bir  44650  e2bir  44653  e3bir  44759  suctrALT  44846  19.21a3con13vVD  44872  3impexpbicomVD  44877  tratrbVD  44881  ssralv2VD  44886  truniALTVD  44898  trintALTVD  44900  undif3VD  44902  csbingVD  44904  onfrALTlem3VD  44907  onfrALTlem2VD  44909  onfrALTVD  44911  csbsngVD  44913  csbxpgVD  44914  csbrngVD  44916  csbunigVD  44918  csbfv12gALTVD  44919  relopabVD  44921  ax6e2ndVD  44928  2uasbanhVD  44931  vk15.4jVD  44934  sspwimp  44938  sspwimpVD  44939  sspwimpcf  44940  sspwimpcfVD  44941  suctrALTcf  44942  suctrALTcfVD  44943  suctrALT3  44944  sspwimpALT  44945  unisnALT  44946  ax6e2ndALT  44950  isosctrlem1ALT  44954  iunconnlem2  44955  prclaxpr  45002  wfaxrep  45011  supminfxrrnmpt  45482  limsuppnflem  45725  limsupubuz  45728  cncfuni  45901  iblcncfioo  45993  stoweidlem14  46029  stoweidlem17  46032  stoweidlem35  46050  stoweidlem57  46072  stirlinglem7  46095  stirlinglem10  46098  fourierdlem54  46175  fourierdlem62  46183  fourierdlem63  46184  fourierdlem65  46186  fourierdlem73  46194  fourierdlem80  46201  fourierdlem82  46203  fourierdlem101  46222  etransclem32  46281  ioorrnopnxr  46322  subsaliuncl  46373  meadjiunlem  46480  ismeannd  46482  voliunsge0lem  46487  volmea  46489  caratheodory  46543  ovnsubaddlem2  46586  hoidmvlelem5  46614  hoiqssbllem2  46638  iinhoiicc  46689  aibandbiaiaiffb  46907  funressnvmo  47057  dfdfat2  47140  afvres  47184  tz6.12-afv  47185  ndmaovass  47218  afv2res  47251  tz6.12-afv2  47252  el1fzopredsuc  47337  zp1modne  47348  fundcmpsurinjimaid  47398  iccpartiltu  47409  iccelpart  47420  lswn0  47431  ichnfimlem  47450  prprelb  47503  evenprm2  47701  dfnbgr6  47843  dfsclnbgr6  47844  isgrtri  47910  lincext1  48371  resinsnALT  48773  tposideq  48788  sepfsepc  48825  isclatd  48872  intubeu  48873  unilbeu  48874  uprcl2  48941  functhincfun  49098  fullthinc  49099  setc2othin  49113