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  851  rnlemOLD  963  syl3an1br  1267  syl3an2br  1268  syl3an3br  1269  nic-axALT  1491  speimfw  1707  sbbii  1718  hbn1fw  1761  exmoeuOLD  2312  exmidne  2672  eueq2  3277  ralun  3686  ssunieq  4280  ax6vsep  4572  ordunidif  4926  unizlim  4994  opelxpi  5031  ndmima  5373  funtpg  5638  dffo2  5799  dff1o2  5821  resdif  5836  f1o00  5848  fvimacnvALT  6000  fvcofneq  6029  exfo  6039  ressnop0  6068  fsnunfv  6101  ovid  6403  ovidig  6404  dfwe2  6601  onminex  6626  nnsuc  6701  1stnpr  6788  2ndnpr  6789  f1stres  6806  f2ndres  6807  1st2val  6810  2nd2val  6811  frxp  6893  soxp  6896  tz7.49  7110  elixpsn  7508  domdifsn  7600  domunsncan  7617  fineqvlem  7734  unblem4  7775  funsnfsupp  7853  ordiso2  7940  domwdom  8000  inf3lem3  8047  trcl  8159  unir1  8231  ssrankr1  8253  pm54.43lem  8380  infxpenlem  8391  ween  8416  acni3  8428  kmlem1  8530  infdif  8589  ackbij1lem1  8600  fin23lem14  8713  fin23lem32  8724  fin23lem40  8731  isfin1-3  8766  axcc2lem  8816  axdc3lem2  8831  axcclem  8837  ac6c4  8861  zornn0g  8885  axdclem2  8900  brdom3  8906  brdom5  8907  brdom4  8908  brdom6disj  8910  konigthlem  8943  pwcfsdom  8958  cfpwsdom  8959  alephom  8960  gruina  9196  grur1  9198  grothomex  9207  grothac  9208  nqpr  9392  axcnre  9541  axpre-sup  9546  ssxr  9654  le2tri3i  9714  0nn0  10810  uzind4  11139  rpnnen1lem5  11212  elfz4  11681  eluzfz  11683  ssfzo12bi  11875  hashgt0elex  12432  hashxplem  12457  hashfun  12461  ffz0iswrd  12534  wrdsymb1  12543  ccatfv0  12566  swrdn0  12618  ccatswrd  12644  repswfsts  12716  cshw1  12753  swrdco  12766  resqrex  13047  fsumsplitsnun  13533  ndvdsadd  13925  gcdcllem1  14008  gcdcllem3  14010  1idssfct  14082  cshwrepswhash1  14445  xpsff1o  14823  clatlem  15598  clatlubcl2  15600  clatglbcl2  15602  xpsmnd  15779  xpsgrp  15999  symg2bas  16228  symgextf  16247  gsmsymgrfix  16258  gsmsymgreqlem2  16261  pmtr3ncom  16306  odlem1  16365  gexlem1  16405  dprdfeq0  16864  dprdfeq0OLD  16871  gsumdixpOLD  17058  gsumdixp  17059  lspcl  17422  cply1mul  18134  psgndiflemB  18431  lindfind  18646  lindsind  18647  lindsind2  18649  lindff1  18650  f1linds  18655  gsumcom3fi  18697  mat1dimscm  18772  dmatmul  18794  mdetdiag  18896  mdetunilem7  18915  mdetunilem9  18917  madurid  18941  fvmptnn04if  19145  tgcl  19265  elcls  19368  opnnei  19415  neiptopnei  19427  cnpnei  19559  cmpcov2  19684  cmpfii  19703  txcnp  19884  xpstps  20074  fbun  20104  isfild  20122  snfil  20128  filcon  20147  isufil2  20172  hauspwpwf1  20251  cnextcn  20330  ustfilxp  20478  ustuqtop4  20510  xpsxms  20800  xpsms  20801  rlmnvc  20974  nmoid  21012  xrsmopn  21080  xrhmeo  21209  cphsqrtcl  21394  iscmet3  21495  rrxcph  21587  iundisj  21721  ioorinv  21748  plyexmo  22471  aalioulem3  22492  dvtaylp  22527  dvradcnv  22578  logtayllem  22796  logtayl  22797  musum  23223  pntlem3  23550  isismt  23677  usgrarnedg  24088  nb3grapr  24157  nb3grapr2  24158  nb3gra2nb  24159  nbcusgra  24167  wlkcpr  24233  2pthlem2  24302  nvnencycllem  24347  wlkiswwlk2lem1  24395  clwwlkel  24497  clwwlkf1  24500  clwlkf1clwwlklem  24553  2wlkonotv  24581  clwlknclwlkdifs  24664  frgra0v  24697  frgra3v  24706  2pthfrgrarn  24713  2pthfrgra  24715  n4cyclfrgra  24722  frgrancvvdeqlem9  24746  frgrawopreglem3  24751  frgraregorufr0  24757  numclwwlk2lem1  24807  subgoablo  25017  ismndo2  25051  rngomndo  25127  sspval  25340  blo3i  25421  ajfval  25428  spanval  25955  cmcmlem  26213  cnvbraval  26733  leopnmid  26761  csmdsymi  26957  chirredlem4  27016  sumdmdlem  27041  ceqsexv2d  27101  iundisjf  27149  ofpreima2  27208  rnct  27239  xrge0infss  27276  iundisjfi  27297  ishashinf  27302  xrpxdivcld  27327  pnfneige0  27597  rrhre  27663  logbid1  27682  esumcocn  27754  hasheuni  27759  sgon  27792  ddemeas  27876  1stmbfm  27899  2ndmbfm  27900  dya2iocct  27919  dya2iocnrect  27920  eulerpartgbij  27979  eulerpartlemgs2  27987  coinflippv  28090  cvmsdisj  28383  problem4  28525  climuzcnv  28540  dfon2lem3  28822  dfon2lem7  28826  sspred  28857  sltval2  29021  nodenselem5  29050  imageval  29185  df3nandALT1  29467  lukshef-ax2  29485  arg-ax  29486  finixpnum  29643  fin2solem  29644  mblfinlem3  29658  itg2addnclem2  29672  itg2addnc  29674  bddiblnc  29690  ftc1anclem6  29700  filnetlem2  29828  heiborlem3  29940  isfld2  30033  igenval2  30094  isfldidl  30096  dmncan2  30105  tsbi3  30174  oprabbi  30202  mpt2bi123f  30203  opabbi  30206  ac6s3f  30211  pellexlem5  30401  rmyabs  30528  jm2.24  30533  islssfgi  30650  pwslnm  30672  dgraaub  30730  infrglb  31168  cncfuni  31253  icccncfext  31254  cncfiooicclem1  31260  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  iblcncfioo  31324  stoweidlem14  31342  stoweidlem17  31345  stoweidlem35  31363  stoweidlem55  31383  stoweidlem57  31385  stoweid  31391  stirlinglem7  31408  stirlinglem10  31411  fourierdlem42  31477  fourierdlem48  31483  fourierdlem50  31485  fourierdlem54  31489  fourierdlem62  31497  fourierdlem63  31498  fourierdlem65  31500  fourierdlem73  31508  fourierdlem76  31511  fourierdlem82  31517  fourierdlem87  31522  fourierdlem101  31536  aibandbiaiaiffb  31585  fnresfnco  31706  dfdfat2  31711  afvres  31752  tz6.12-afv  31753  ndmaovass  31786  2f1fvneq  31802  el2fzo  31834  fzoopth  31835  lswn0  31838  spthdifv  31847  lincext1  32154  3impexpbicom  32318  ee3bir  32369  vk15.4j  32395  onfrALTlem2  32416  ax6e2nd  32429  dfvd1impr  32451  dfvd2impr  32488  e1bir  32514  e2bir  32517  e3bir  32634  suctrALT  32724  19.21a3con13vVD  32750  3impexpbicomVD  32755  tratrbVD  32759  ssralv2VD  32764  truniALTVD  32776  trintALTVD  32778  undif3VD  32780  onfrALTlem3VD  32785  onfrALTlem2VD  32787  onfrALTVD  32789  relopabVD  32799  ax6e2ndVD  32806  2uasbanhVD  32809  vk15.4jVD  32812  sspwimp  32816  sspwimpVD  32817  sspwimpcf  32818  sspwimpcfVD  32819  suctrALTcf  32820  suctrALTcfVD  32821  suctrALT3  32822  sspwimpALT  32823  unisnALT  32824  ax6e2ndALT  32828  isosctrlem1ALT  32832  iunconlem2  32833  bnj1136  33150  bnj1175  33157  bnj1408  33189  sylbbr  33230  sylbb1  33231  sylbb2  33232  sylancl3  33268  bj-andnotim  33276  bj-modalbe  33341  bj-projval  33653  bj-2uplex  33679  lsat0cv  33848  pclfinclN  34764  docavalN  35938  djavalN  35950  dochval  36166  djhval  36213  dochexmidlem8  36282  dochkr1  36293  dochkr1OLDN  36294  hdmap1fval  36612  xptrrel  36803  bj-frege52a  36886  bj-frege55lem1a  36893  frege54cor1c  36925  frege58newc  36931