Theorem biimpri 206

Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (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  470  sylan2br  473  pm3.11  496  orbi2i  516  pm2.31  522  simplbi2  622  dfbi  624  pm2.85  844  rnlem  951  syl3an1br  1252  syl3an2br  1253  syl3an3br  1254  3impexpbicom  1416  nic-axALT  1486  sbbii  1712  hbn1fw  1755  exmoeuOLD  2295  eueq2  3130  ralun  3535  ssunieq  4123  ax6vsep  4414  ordunidif  4763  unizlim  4831  opelxpi  4867  ndmima  5202  funtpg  5465  dffo2  5621  dff1o2  5643  resdif  5658  f1o00  5670  fvimacnvALT  5819  fvcofneq  5848  exfo  5858  ressnop0  5886  fsnunfv  5915  ovid  6206  ovidig  6207  dfwe2  6392  onminex  6417  nnsuc  6492  1stnpr  6580  2ndnpr  6581  f1stres  6597  f2ndres  6598  1st2val  6601  2nd2val  6602  frxp  6681  soxp  6684  tz7.49  6896  elixpsn  7298  domdifsn  7390  domunsncan  7407  fineqvlem  7523  unblem4  7563  funsnfsupp  7640  ordiso2  7725  domwdom  7785  inf3lem3  7832  trcl  7944  unir1  8016  ssrankr1  8038  pm54.43lem  8165  infxpenlem  8176  ween  8201  acni3  8213  kmlem1  8315  infdif  8374  ackbij1lem1  8385  fin23lem14  8498  fin23lem32  8509  fin23lem40  8516  isfin1-3  8551  axcc2lem  8601  axdc3lem2  8616  axcclem  8622  ac6c4  8646  zornn0g  8670  axdclem2  8685  brdom3  8691  brdom5  8692  brdom4  8693  brdom6disj  8695  konigthlem  8728  pwcfsdom  8743  cfpwsdom  8744  alephom  8745  gruina  8981  grur1  8983  grothomex  8992  grothac  8993  nqpr  9179  axcnre  9327  axpre-sup  9332  ssxr  9440  le2tri3i  9500  0nn0  10590  uzind4  10908  rpnnen1lem5  10979  elfz4  11442  eluzfz  11444  ssfzo12bi  11618  hashgt0elex  12155  hashxplem  12191  hashfun  12195  ffz0iswrd  12251  wrdsymb1  12258  ccatfv0  12278  swrdn0  12320  ccatswrd  12346  repswfsts  12415  cshw1  12452  swrdco  12461  resqrex  12736  ndvdsadd  13608  gcdcllem1  13691  gcdcllem3  13693  1idssfct  13765  cshwrepswhash1  14125  xpsff1o  14502  clatlem  15277  clatlubcl2  15279  clatglbcl2  15281  xpsmnd  15457  xpsgrp  15667  symg2bas  15896  symgextf  15915  gsmsymgrfix  15926  gsmsymgreqlem2  15929  pmtr3ncom  15974  odlem1  16031  gexlem1  16071  dprdfeq0  16502  dprdfeq0OLD  16509  gsumdixpOLD  16690  gsumdixp  16691  lspcl  17035  psgndiflemB  17930  lindfind  18145  lindsind  18146  lindsind2  18148  lindff1  18149  f1linds  18154  gsumcom3fi  18200  mdetunilem7  18324  mdetunilem9  18326  madurid  18350  tgcl  18474  elcls  18577  opnnei  18624  neiptopnei  18636  cnpnei  18768  cmpcov2  18893  cmpfii  18912  txcnp  19093  xpstps  19283  fbun  19313  isfild  19331  snfil  19337  filcon  19356  isufil2  19381  hauspwpwf1  19460  cnextcn  19539  ustfilxp  19687  ustuqtop4  19719  xpsxms  20009  xpsms  20010  rlmnvc  20183  nmoid  20221  xrsmopn  20289  xrhmeo  20418  cphsqrcl  20603  iscmet3  20704  rrxcph  20796  iundisj  20929  ioorinv  20956  plyexmo  21722  aalioulem3  21743  dvtaylp  21778  dvradcnv  21829  logtayllem  22047  logtayl  22048  musum  22474  pntlem3  22801  usgrarnedg  23222  nb3grapr  23280  nb3grapr2  23281  nb3gra2nb  23282  nbcusgra  23290  2pthlem2  23414  nvnencycllem  23448  subgoablo  23717  ismndo2  23751  rngomndo  23827  sspval  24040  blo3i  24121  ajfval  24128  spanval  24655  cmcmlem  24913  cnvbraval  25433  leopnmid  25461  csmdsymi  25657  chirredlem4  25716  sumdmdlem  25741  ceqsexv2d  25801  iundisjf  25850  ofpreima2  25904  rnct  25935  iundisjfi  25997  ishashinf  26002  xrpxdivcld  26027  pnfneige0  26301  rrhre  26367  logbid1  26377  esumcocn  26449  hasheuni  26454  sgon  26487  ddemeas  26572  1stmbfm  26595  2ndmbfm  26596  dya2iocct  26615  dya2iocnrect  26616  eulerpartgbij  26669  eulerpartlemgs2  26677  coinflippv  26780  cvmsdisj  27073  problem4  27215  climuzcnv  27229  dfon2lem3  27511  dfon2lem7  27515  sspred  27546  sltval2  27710  nodenselem5  27739  imageval  27874  df3nandALT1  28156  lukshef-ax2  28175  arg-ax  28176  finixpnum  28323  fin2solem  28324  mblfinlem3  28339  itg2addnclem2  28353  itg2addnc  28355  bddiblnc  28371  ftc1anclem6  28381  filnetlem2  28509  heiborlem3  28621  isfld2  28714  igenval2  28775  isfldidl  28777  dmncan2  28786  tsbi3  28855  oprabbi  28883  mpt2bi123f  28884  opabbi  28887  ac6s3f  28892  pellexlem5  29083  rmyabs  29210  jm2.24  29215  islssfgi  29334  pwslnm  29356  dgraaub  29414  infrglb  29680  stoweidlem14  29718  stoweidlem17  29721  stoweidlem35  29739  stoweidlem55  29759  stoweidlem57  29761  stoweid  29767  stirlinglem7  29784  stirlinglem10  29787  aibandbiaiaiffb  29818  fnresfnco  29941  dfdfat2  29946  afvres  29987  tz6.12-afv  29988  ndmaovass  30021  2f1fvneq  30052  el2fzo  30121  fzoopth  30122  fsumsplitsnun  30151  lswn0  30167  wlkcpr  30199  spthdifv  30208  wlkiswwlk2lem1  30234  2wlkonotv  30305  clwwlkel  30364  clwwlkf1  30367  clwlkf1clwwlklem  30431  clwlknclwlkdifs  30487  frgra0v  30494  frgra3v  30503  2pthfrgrarn  30510  2pthfrgra  30512  n4cyclfrgra  30519  frgrancvvdeqlem9  30543  frgrawopreglem3  30548  frgraregorufr0  30554  numclwwlk2lem1  30604  mat1dimscm  30737  dmatmul  30742  mdetdiag  30760  lincext1  30812  ee3bir  31023  vk15.4j  31049  onfrALTlem2  31070  ax6e2nd  31083  dfvd1impr  31106  dfvd2impr  31143  e1bir  31169  e2bir  31172  e3bir  31289  suctrALT  31379  19.21a3con13vVD  31405  3impexpbicomVD  31410  tratrbVD  31414  ssralv2VD  31419  truniALTVD  31431  trintALTVD  31433  undif3VD  31435  onfrALTlem3VD  31440  onfrALTlem2VD  31442  onfrALTVD  31444  relopabVD  31454  ax6e2ndVD  31461  2uasbanhVD  31464  vk15.4jVD  31467  sspwimp  31471  sspwimpVD  31472  sspwimpcf  31473  sspwimpcfVD  31474  suctrALTcf  31475  suctrALTcfVD  31476  suctrALT3  31477  sspwimpALT  31478  unisnALT  31479  ax6e2ndALT  31483  isosctrlem1ALT  31487  iunconlem2  31488  bnj1136  31805  bnj1175  31812  bnj1408  31844  sylbbr  31881  sylbb1  31882  sylbb2  31883  sylancl3  31889  bj-andnotim  31891  bj-projval  32187  bj-2uplex  32213  lsat0cv  32366  pclfinclN  33282  docavalN  34456  djavalN  34468  dochval  34684  djhval  34731  dochexmidlem8  34800  dochkr1  34811  dochkr1OLDN  34812  hdmap1fval  35130