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  296  pm2.54  372  sylanbr  471  sylan2br  474  pm3.11  497  orbi2i  517  pm2.31  523  simplbi2  623  dfbi  627  pm2.85  851  rnlemOLD  963  syl3an1br  1265  syl3an2br  1266  syl3an3br  1267  nic-axALT  1514  speimfw  1743  sbbii  1754  exmidne  2587  eueq2  3198  ralun  3600  euelss  3710  ssunieq  4197  ax6vsep  4492  ordunidif  4840  unizlim  4908  opelxpi  4945  ndmima  5285  ndmimaOLD  5286  funtpg  5546  dffo2  5707  dff1o2  5729  resdif  5744  f1o00  5756  fvimacnvALT  5908  fvcofneq  5941  exfo  5951  ressnop0  5980  fsnunfv  6013  ovid  6318  ovidig  6319  dfwe2  6516  onminex  6541  nnsuc  6616  1stnpr  6703  2ndnpr  6704  f1stres  6721  f2ndres  6722  1st2val  6725  2nd2val  6726  frxp  6809  soxp  6812  tz7.49  7028  elixpsn  7427  domdifsn  7519  domunsncan  7536  fineqvlem  7650  unblem4  7690  funsnfsupp  7768  ordiso2  7855  domwdom  7915  inf3lem3  7961  trcl  8072  unir1  8144  ssrankr1  8166  pm54.43lem  8293  infxpenlem  8304  ween  8329  acni3  8341  kmlem1  8443  infdif  8502  ackbij1lem1  8513  fin23lem14  8626  fin23lem32  8637  fin23lem40  8644  isfin1-3  8679  axcc2lem  8729  axdc3lem2  8744  axcclem  8750  ac6c4  8774  zornn0g  8798  axdclem2  8813  brdom3  8819  brdom5  8820  brdom4  8821  brdom6disj  8823  konigthlem  8856  pwcfsdom  8871  cfpwsdom  8872  alephom  8873  gruina  9107  grur1  9109  grothomex  9118  grothac  9119  nqpr  9303  axcnre  9452  axpre-sup  9457  ssxr  9565  le2tri3i  9625  0nn0  10727  uzind4  11059  rpnnen1lem5  11131  elfz4  11602  eluzfz  11604  ssfzo12bi  11806  hashgt0elex  12370  hashxplem  12395  hashfun  12399  ffz0iswrd  12476  wrdsymb1  12486  ccatfv0  12510  lswccats1fst  12548  ccatswrd  12592  repswfsts  12664  cshw1  12701  swrdco  12714  cotr2g  12814  xptrrel  12818  trclun  12852  resqrex  13086  fsumsplitsnun  13572  ndvdsadd  14068  gcdcllem1  14151  gcdcllem3  14153  1idssfct  14225  cshwrepswhash1  14589  xpsff1o  14975  initoeu2  15412  clatlem  15858  clatlubcl2  15860  clatglbcl2  15862  xpsmnd  16077  sgrp2rid2  16161  xpsgrp  16306  symg2bas  16540  symgextf  16559  gsmsymgrfix  16570  gsmsymgreqlem2  16573  pmtr3ncom  16617  odlem1  16676  gexlem1  16716  dprdfeq0  17175  dprdfeq0OLD  17182  gsumdixpOLD  17370  gsumdixp  17371  lspcl  17735  cply1mul  18448  psgndiflemB  18727  lindfind  18936  lindsind  18937  lindsind2  18939  lindff1  18940  f1linds  18945  gsumcom3fi  18987  mat1dimscm  19062  dmatmul  19084  mdetdiag  19186  mdetunilem7  19205  mdetunilem9  19207  madurid  19231  fvmptnn04if  19435  tgcl  19556  elcls  19660  opnnei  19707  neiptopnei  19719  cnpnei  19851  cmpcov2  19976  cmpfii  19995  txcnp  20206  xpstps  20396  fbun  20426  isfild  20444  snfil  20450  filcon  20469  isufil2  20494  hauspwpwf1  20573  cnextcn  20652  ustfilxp  20800  ustuqtop4  20832  xpsxms  21122  xpsms  21123  rlmnvc  21296  nmoid  21334  xrsmopn  21402  xrhmeo  21531  cphsqrtcl  21716  iscmet3  21817  rrxcph  21909  iundisj  22043  ioorinv  22070  plyexmo  22794  aalioulem3  22815  dvtaylp  22850  dvradcnv  22901  logtayllem  23127  logtayl  23128  logbid1  23226  logbchbase  23229  relogbcxpb  23245  logbmpt  23246  logbfval  23248  musum  23584  pntlem3  23911  usgrarnedg  24505  nb3grapr  24574  nb3grapr2  24575  nb3gra2nb  24576  nbcusgra  24584  wlkcpr  24650  2pthlem2  24719  nvnencycllem  24764  wlkiswwlk2lem1  24812  clwwlkel  24914  clwwlkf1  24917  clwlkf1clwwlklem  24970  2wlkonotv  24998  clwlknclwlkdifs  25081  frgra0v  25114  frgra3v  25123  2pthfrgrarn  25130  2pthfrgra  25132  n4cyclfrgra  25139  frgrancvvdeqlem9  25162  frgrawopreglem3  25167  frgraregorufr0  25173  numclwwlk2lem1  25223  subgoablo  25430  ismndo2  25464  rngomndo  25540  sspval  25753  blo3i  25834  ajfval  25841  spanval  26368  cmcmlem  26626  cnvbraval  27145  leopnmid  27173  csmdsymi  27369  chirredlem4  27428  sumdmdlem  27453  ceqsexv2d  27514  iundisjf  27578  elsnxp  27603  rnct  27688  padct  27695  xrge0infss  27730  iundisjfi  27754  ishashinf  27759  xrpxdivcld  27784  pnfneige0  28087  rrhre  28152  esumcocn  28228  hasheuni  28233  sgon  28273  sigapildsys  28307  ddemeas  28364  1stmbfm  28387  2ndmbfm  28388  dya2iocct  28407  dya2iocnrect  28408  eulerpartgbij  28494  eulerpartlemgs2  28502  coinflippv  28605  cvmsdisj  28904  mrsubvrs  29071  mppspstlem  29120  problem4  29211  climuzcnv  29226  dfon2lem3  29382  dfon2lem7  29386  sspred  29417  sltval2  29581  nodenselem5  29610  imageval  29733  df3nandALT1  30015  lukshef-ax2  30033  arg-ax  30034  finixpnum  30203  fin2solem  30204  mblfinlem3  30218  itg2addnclem2  30233  itg2addnc  30235  bddiblnc  30251  ftc1anclem6  30261  filnetlem2  30363  heiborlem3  30475  isfld2  30568  igenval2  30629  isfldidl  30631  dmncan2  30640  oprabbi  30736  mpt2bi123f  30737  opabbi  30740  ac6s3f  30745  pellexlem5  30934  rmyabs  31061  jm2.24  31066  islssfgi  31184  pwslnm  31206  dgraaub  31265  infrglb  31750  cncfuni  31855  iblcncfioo  31943  stoweidlem14  31962  stoweidlem17  31965  stoweidlem35  31983  stoweidlem57  32005  stirlinglem7  32028  stirlinglem10  32031  fourierdlem54  32109  fourierdlem62  32117  fourierdlem63  32118  fourierdlem65  32120  fourierdlem73  32128  fourierdlem80  32135  fourierdlem82  32137  fourierdlem101  32156  etransclem32  32215  aibandbiaiaiffb  32256  fnresfnco  32377  dfdfat2  32382  afvres  32423  tz6.12-afv  32424  ndmaovass  32457  lswn0  32554  ccatpfx  32584  2f1fvneq  32628  fzoopth  32660  spthdifv  32670  lincext1  33255  3impexpbicom  33554  ee3bir  33605  vk15.4j  33631  onfrALTlem2  33658  ax6e2nd  33671  dfvd1impr  33693  dfvd2impr  33730  e1bir  33756  e2bir  33759  e3bir  33876  suctrALT  33972  19.21a3con13vVD  33998  3impexpbicomVD  34003  tratrbVD  34008  ssralv2VD  34013  truniALTVD  34025  trintALTVD  34027  undif3VD  34029  onfrALTlem3VD  34034  onfrALTlem2VD  34036  onfrALTVD  34038  relopabVD  34048  ax6e2ndVD  34055  2uasbanhVD  34058  vk15.4jVD  34061  sspwimp  34065  sspwimpVD  34066  sspwimpcf  34067  sspwimpcfVD  34068  suctrALTcf  34069  suctrALTcfVD  34070  suctrALT3  34071  sspwimpALT  34072  unisnALT  34073  ax6e2ndALT  34077  isosctrlem1ALT  34081  iunconlem2  34082  bnj1136  34400  bnj1175  34407  bnj1408  34439  sylbbr  34480  sylbb1  34481  sylbb2  34482  sylancl3  34516  bj-andnotim  34524  bj-modalbe  34588  bj-2uplex  34928  lsat0cv  35171  pclfinclN  36087  docavalN  37263  djavalN  37275  dochval  37491  djhval  37538  dochexmidlem8  37607  dochkr1  37618  dochkr1OLDN  37619  hdmap1fval  37937  frege55lem1a  38365  frege70  38432