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  849  rnlem  956  syl3an1br  1257  syl3an2br  1258  syl3an3br  1259  nic-axALT  1481  sbbii  1707  hbn1fw  1750  exmoeuOLD  2290  eueq2  3133  ralun  3538  ssunieq  4126  ax6vsep  4417  ordunidif  4767  unizlim  4835  opelxpi  4871  ndmima  5205  funtpg  5468  dffo2  5624  dff1o2  5646  resdif  5661  f1o00  5673  fvimacnvALT  5822  fvcofneq  5851  exfo  5861  ressnop0  5889  fsnunfv  5918  ovid  6207  ovidig  6208  dfwe2  6393  onminex  6418  nnsuc  6493  1stnpr  6581  2ndnpr  6582  f1stres  6598  f2ndres  6599  1st2val  6602  2nd2val  6603  frxp  6682  soxp  6685  tz7.49  6900  elixpsn  7302  domdifsn  7394  domunsncan  7411  fineqvlem  7527  unblem4  7567  funsnfsupp  7644  ordiso2  7729  domwdom  7789  inf3lem3  7836  trcl  7948  unir1  8020  ssrankr1  8042  pm54.43lem  8169  infxpenlem  8180  ween  8205  acni3  8217  kmlem1  8319  infdif  8378  ackbij1lem1  8389  fin23lem14  8502  fin23lem32  8513  fin23lem40  8520  isfin1-3  8555  axcc2lem  8605  axdc3lem2  8620  axcclem  8626  ac6c4  8650  zornn0g  8674  axdclem2  8689  brdom3  8695  brdom5  8696  brdom4  8697  brdom6disj  8699  konigthlem  8732  pwcfsdom  8747  cfpwsdom  8748  alephom  8749  gruina  8985  grur1  8987  grothomex  8996  grothac  8997  nqpr  9183  axcnre  9331  axpre-sup  9336  ssxr  9444  le2tri3i  9504  0nn0  10594  uzind4  10912  rpnnen1lem5  10983  elfz4  11446  eluzfz  11448  ssfzo12bi  11622  hashgt0elex  12159  hashxplem  12195  hashfun  12199  ffz0iswrd  12255  wrdsymb1  12262  ccatfv0  12282  swrdn0  12324  ccatswrd  12350  repswfsts  12419  cshw1  12456  swrdco  12465  resqrex  12740  ndvdsadd  13612  gcdcllem1  13695  gcdcllem3  13697  1idssfct  13769  cshwrepswhash1  14129  xpsff1o  14506  clatlem  15281  clatlubcl2  15283  clatglbcl2  15285  xpsmnd  15461  xpsgrp  15674  symg2bas  15903  symgextf  15922  gsmsymgrfix  15933  gsmsymgreqlem2  15936  pmtr3ncom  15981  odlem1  16038  gexlem1  16078  dprdfeq0  16512  dprdfeq0OLD  16519  gsumdixpOLD  16700  gsumdixp  16701  lspcl  17057  psgndiflemB  18030  lindfind  18245  lindsind  18246  lindsind2  18248  lindff1  18249  f1linds  18254  gsumcom3fi  18300  mdetunilem7  18424  mdetunilem9  18426  madurid  18450  tgcl  18574  elcls  18677  opnnei  18724  neiptopnei  18736  cnpnei  18868  cmpcov2  18993  cmpfii  19012  txcnp  19193  xpstps  19383  fbun  19413  isfild  19431  snfil  19437  filcon  19456  isufil2  19481  hauspwpwf1  19560  cnextcn  19639  ustfilxp  19787  ustuqtop4  19819  xpsxms  20109  xpsms  20110  rlmnvc  20283  nmoid  20321  xrsmopn  20389  xrhmeo  20518  cphsqrcl  20703  iscmet3  20804  rrxcph  20896  iundisj  21029  ioorinv  21056  plyexmo  21779  aalioulem3  21800  dvtaylp  21835  dvradcnv  21886  logtayllem  22104  logtayl  22105  musum  22531  pntlem3  22858  usgrarnedg  23303  nb3grapr  23361  nb3grapr2  23362  nb3gra2nb  23363  nbcusgra  23371  2pthlem2  23495  nvnencycllem  23529  subgoablo  23798  ismndo2  23832  rngomndo  23908  sspval  24121  blo3i  24202  ajfval  24209  spanval  24736  cmcmlem  24994  cnvbraval  25514  leopnmid  25542  csmdsymi  25738  chirredlem4  25797  sumdmdlem  25822  ceqsexv2d  25882  iundisjf  25931  ofpreima2  25985  rnct  26016  xrge0infss  26053  iundisjfi  26080  ishashinf  26085  xrpxdivcld  26110  pnfneige0  26381  rrhre  26447  logbid1  26457  esumcocn  26529  hasheuni  26534  sgon  26567  ddemeas  26652  1stmbfm  26675  2ndmbfm  26676  dya2iocct  26695  dya2iocnrect  26696  eulerpartgbij  26755  eulerpartlemgs2  26763  coinflippv  26866  cvmsdisj  27159  problem4  27301  climuzcnv  27316  dfon2lem3  27598  dfon2lem7  27602  sspred  27633  sltval2  27797  nodenselem5  27826  imageval  27961  df3nandALT1  28243  lukshef-ax2  28261  arg-ax  28262  finixpnum  28414  fin2solem  28415  mblfinlem3  28430  itg2addnclem2  28444  itg2addnc  28446  bddiblnc  28462  ftc1anclem6  28472  filnetlem2  28600  heiborlem3  28712  isfld2  28805  igenval2  28866  isfldidl  28868  dmncan2  28877  tsbi3  28946  oprabbi  28974  mpt2bi123f  28975  opabbi  28978  ac6s3f  28983  pellexlem5  29174  rmyabs  29301  jm2.24  29306  islssfgi  29425  pwslnm  29447  dgraaub  29505  infrglb  29771  stoweidlem14  29809  stoweidlem17  29812  stoweidlem35  29830  stoweidlem55  29850  stoweidlem57  29852  stoweid  29858  stirlinglem7  29875  stirlinglem10  29878  aibandbiaiaiffb  29909  fnresfnco  30032  dfdfat2  30037  afvres  30078  tz6.12-afv  30079  ndmaovass  30112  2f1fvneq  30143  el2fzo  30212  fzoopth  30213  fsumsplitsnun  30242  lswn0  30258  wlkcpr  30290  spthdifv  30299  wlkiswwlk2lem1  30325  2wlkonotv  30396  clwwlkel  30455  clwwlkf1  30458  clwlkf1clwwlklem  30522  clwlknclwlkdifs  30578  frgra0v  30585  frgra3v  30594  2pthfrgrarn  30601  2pthfrgra  30603  n4cyclfrgra  30610  frgrancvvdeqlem9  30634  frgrawopreglem3  30639  frgraregorufr0  30645  numclwwlk2lem1  30695  mat1dimscm  30871  dmatmul  30876  mdetdiag  30936  lincext1  30988  3impexpbicom  31156  ee3bir  31207  vk15.4j  31233  onfrALTlem2  31254  ax6e2nd  31267  dfvd1impr  31289  dfvd2impr  31326  e1bir  31352  e2bir  31355  e3bir  31472  suctrALT  31562  19.21a3con13vVD  31588  3impexpbicomVD  31593  tratrbVD  31597  ssralv2VD  31602  truniALTVD  31614  trintALTVD  31616  undif3VD  31618  onfrALTlem3VD  31623  onfrALTlem2VD  31625  onfrALTVD  31627  relopabVD  31637  ax6e2ndVD  31644  2uasbanhVD  31647  vk15.4jVD  31650  sspwimp  31654  sspwimpVD  31655  sspwimpcf  31656  sspwimpcfVD  31657  suctrALTcf  31658  suctrALTcfVD  31659  suctrALT3  31660  sspwimpALT  31661  unisnALT  31662  ax6e2ndALT  31666  isosctrlem1ALT  31670  iunconlem2  31671  bnj1136  31988  bnj1175  31995  bnj1408  32027  sylbbr  32068  sylbb1  32069  sylbb2  32070  sylancl3  32106  bj-andnotim  32114  bj-modalbe  32177  bj-projval  32489  bj-2uplex  32515  lsat0cv  32678  pclfinclN  33594  docavalN  34768  djavalN  34780  dochval  34996  djhval  35043  dochexmidlem8  35112  dochkr1  35123  dochkr1OLDN  35124  hdmap1fval  35442