Theorem biimpri 206

Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)

Hypothesis

Ref	Expression
biimpri.1	|- ( ph <-> ps )

Assertion

Ref	Expression
biimpri	|- ( ps -> ph )

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 |- ( ph <-> ps )
2	1	bicomi 202	. 2 |- ( ps <-> ph )
3	2	biimpi 194	1 |- ( ps -> ph )

Syntax hints:   -> wi 4   <-> wb 184

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 185

This theorem is referenced by:  mpbir  209  sylibr  212  sylbir  213  syl5bir  218  syl6ibr  227  bitri  249  mtbi  298  pm2.54  374  sylanbr  473  sylan2br  476  pm3.11  499  orbi2i  519  pm2.31  525  simplbi2  625  dfbi  629  pm2.85  853  rnlemOLD  965  syl3an1br  1268  syl3an2br  1269  syl3an3br  1270  nic-axALT  1494  speimfw  1722  sbbii  1733  exmidne  2648  eueq2  3259  ralun  3671  ssunieq  4269  ax6vsep  4562  ordunidif  4916  unizlim  4984  opelxpi  5021  ndmima  5363  funtpg  5628  dffo2  5789  dff1o2  5811  resdif  5826  f1o00  5838  fvimacnvALT  5991  fvcofneq  6024  exfo  6034  ressnop0  6063  fsnunfv  6096  ovid  6404  ovidig  6405  dfwe2  6602  onminex  6627  nnsuc  6702  1stnpr  6789  2ndnpr  6790  f1stres  6807  f2ndres  6808  1st2val  6811  2nd2val  6812  frxp  6895  soxp  6898  tz7.49  7112  elixpsn  7510  domdifsn  7602  domunsncan  7619  fineqvlem  7736  unblem4  7777  funsnfsupp  7855  ordiso2  7943  domwdom  8003  inf3lem3  8050  trcl  8162  unir1  8234  ssrankr1  8256  pm54.43lem  8383  infxpenlem  8394  ween  8419  acni3  8431  kmlem1  8533  infdif  8592  ackbij1lem1  8603  fin23lem14  8716  fin23lem32  8727  fin23lem40  8734  isfin1-3  8769  axcc2lem  8819  axdc3lem2  8834  axcclem  8840  ac6c4  8864  zornn0g  8888  axdclem2  8903  brdom3  8909  brdom5  8910  brdom4  8911  brdom6disj  8913  konigthlem  8946  pwcfsdom  8961  cfpwsdom  8962  alephom  8963  gruina  9199  grur1  9201  grothomex  9210  grothac  9211  nqpr  9395  axcnre  9544  axpre-sup  9549  ssxr  9657  le2tri3i  9717  0nn0  10817  uzind4  11150  rpnnen1lem5  11223  elfz4  11692  eluzfz  11694  ssfzo12bi  11889  hashgt0elex  12448  hashxplem  12473  hashfun  12477  ffz0iswrd  12550  wrdsymb1  12560  ccatfv0  12583  swrdn0  12637  ccatswrd  12663  repswfsts  12735  cshw1  12772  swrdco  12785  resqrex  13066  fsumsplitsnun  13552  ndvdsadd  14048  gcdcllem1  14131  gcdcllem3  14133  1idssfct  14205  cshwrepswhash1  14569  xpsff1o  14947  clatlem  15720  clatlubcl2  15722  clatglbcl2  15724  xpsmnd  15939  sgrp2rid2  16023  xpsgrp  16168  symg2bas  16402  symgextf  16421  gsmsymgrfix  16432  gsmsymgreqlem2  16435  pmtr3ncom  16479  odlem1  16538  gexlem1  16578  dprdfeq0  17041  dprdfeq0OLD  17048  gsumdixpOLD  17236  gsumdixp  17237  lspcl  17601  cply1mul  18314  psgndiflemB  18614  lindfind  18829  lindsind  18830  lindsind2  18832  lindff1  18833  f1linds  18838  gsumcom3fi  18880  mat1dimscm  18955  dmatmul  18977  mdetdiag  19079  mdetunilem7  19098  mdetunilem9  19100  madurid  19124  fvmptnn04if  19328  tgcl  19449  elcls  19552  opnnei  19599  neiptopnei  19611  cnpnei  19743  cmpcov2  19868  cmpfii  19887  txcnp  20099  xpstps  20289  fbun  20319  isfild  20337  snfil  20343  filcon  20362  isufil2  20387  hauspwpwf1  20466  cnextcn  20545  ustfilxp  20693  ustuqtop4  20725  xpsxms  21015  xpsms  21016  rlmnvc  21189  nmoid  21227  xrsmopn  21295  xrhmeo  21424  cphsqrtcl  21609  iscmet3  21710  rrxcph  21802  iundisj  21936  ioorinv  21963  plyexmo  22687  aalioulem3  22708  dvtaylp  22743  dvradcnv  22794  logtayllem  23018  logtayl  23019  musum  23445  pntlem3  23772  usgrarnedg  24362  nb3grapr  24431  nb3grapr2  24432  nb3gra2nb  24433  nbcusgra  24441  wlkcpr  24507  2pthlem2  24576  nvnencycllem  24621  wlkiswwlk2lem1  24669  clwwlkel  24771  clwwlkf1  24774  clwlkf1clwwlklem  24827  2wlkonotv  24855  clwlknclwlkdifs  24938  frgra0v  24971  frgra3v  24980  2pthfrgrarn  24987  2pthfrgra  24989  n4cyclfrgra  24996  frgrancvvdeqlem9  25019  frgrawopreglem3  25024  frgraregorufr0  25030  numclwwlk2lem1  25080  subgoablo  25291  ismndo2  25325  rngomndo  25401  sspval  25614  blo3i  25695  ajfval  25702  spanval  26229  cmcmlem  26487  cnvbraval  27007  leopnmid  27035  csmdsymi  27231  chirredlem4  27290  sumdmdlem  27315  ceqsexv2d  27375  iundisjf  27426  rnct  27517  xrge0infss  27558  iundisjfi  27579  ishashinf  27584  xrpxdivcld  27609  pnfneige0  27911  rrhre  27977  logbid1  27992  esumcocn  28064  hasheuni  28069  sgon  28102  ddemeas  28186  1stmbfm  28209  2ndmbfm  28210  dya2iocct  28229  dya2iocnrect  28230  eulerpartgbij  28289  eulerpartlemgs2  28297  coinflippv  28400  cvmsdisj  28693  mrsubvrs  28860  mppspstlem  28909  problem4  29000  climuzcnv  29015  dfon2lem3  29193  dfon2lem7  29197  sspred  29228  sltval2  29392  nodenselem5  29421  imageval  29556  df3nandALT1  29838  lukshef-ax2  29856  arg-ax  29857  finixpnum  30014  fin2solem  30015  mblfinlem3  30029  itg2addnclem2  30043  itg2addnc  30045  bddiblnc  30061  ftc1anclem6  30071  filnetlem2  30173  heiborlem3  30285  isfld2  30378  igenval2  30439  isfldidl  30441  dmncan2  30450  oprabbi  30546  mpt2bi123f  30547  opabbi  30550  ac6s3f  30555  pellexlem5  30745  rmyabs  30872  jm2.24  30877  islssfgi  30994  pwslnm  31016  dgraaub  31073  infrglb  31538  cncfuni  31643  iblcncfioo  31731  stoweidlem14  31750  stoweidlem17  31753  stoweidlem35  31771  stoweidlem57  31793  stirlinglem7  31816  stirlinglem10  31819  fourierdlem54  31897  fourierdlem62  31905  fourierdlem63  31906  fourierdlem65  31908  fourierdlem73  31916  fourierdlem80  31923  fourierdlem82  31925  fourierdlem101  31944  aibandbiaiaiffb  32044  fnresfnco  32165  dfdfat2  32170  afvres  32211  tz6.12-afv  32212  ndmaovass  32245  2f1fvneq  32261  el2fzo  32293  fzoopth  32294  lswn0  32297  spthdifv  32306  lincext1  32925  3impexpbicom  33089  ee3bir  33140  vk15.4j  33166  onfrALTlem2  33186  ax6e2nd  33199  dfvd1impr  33221  dfvd2impr  33258  e1bir  33284  e2bir  33287  e3bir  33404  suctrALT  33494  19.21a3con13vVD  33520  3impexpbicomVD  33525  tratrbVD  33529  ssralv2VD  33534  truniALTVD  33546  trintALTVD  33548  undif3VD  33550  onfrALTlem3VD  33555  onfrALTlem2VD  33557  onfrALTVD  33559  relopabVD  33569  ax6e2ndVD  33576  2uasbanhVD  33579  vk15.4jVD  33582  sspwimp  33586  sspwimpVD  33587  sspwimpcf  33588  sspwimpcfVD  33589  suctrALTcf  33590  suctrALTcfVD  33591  suctrALT3  33592  sspwimpALT  33593  unisnALT  33594  ax6e2ndALT  33598  isosctrlem1ALT  33602  iunconlem2  33603  bnj1136  33921  bnj1175  33928  bnj1408  33960  sylbbr  34001  sylbb1  34002  sylbb2  34003  sylancl3  34052  bj-andnotim  34060  bj-modalbe  34124  bj-2uplex  34463  lsat0cv  34633  pclfinclN  35549  docavalN  36725  djavalN  36737  dochval  36953  djhval  37000  dochexmidlem8  37069  dochkr1  37080  dochkr1OLDN  37081  hdmap1fval  37399  xptrrel  37603  cotr2g  37614  bj-frege55lem1a  37713