Theorem biimpri 209

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 201. (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 205	. 2 |- ( ps <-> ph )
3	2	biimpi 197	1 |- ( ps -> ph )

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

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 188

This theorem is referenced by:  mpbir  212  sylibr  215  sylbir  216  syl5bir  221  syl6ibr  230  bitri  252  mtbi  299  pm2.54  375  sylanbr  475  sylan2br  478  pm3.11  501  orbi2i  521  pm2.31  527  simplbi2  629  dfbi  633  pm2.85  861  rnlemOLD  973  syl3an1br  1303  syl3an2br  1304  syl3an3br  1305  had1  1499  nic-axALT  1551  speimfw  1786  sbbii  1797  exmidne  2605  eueq2  3182  ralun  3586  euelss  3698  ssunieq  4191  ax6vsep  4488  opelxpi  4823  ndmima  5162  ndmimaOLD  5163  elsnxp  5335  sspred  5345  ordunidif  5428  unizlim  5496  funtpg  5589  dffo2  5752  dff1o2  5774  resdif  5789  f1o00  5802  fvimacnvALT  5955  fvcofneq  5984  exfo  5994  ressnop0  6025  fsnunfv  6058  ovid  6366  ovidig  6367  dfwe2  6561  onminex  6587  nnsuc  6662  1stnpr  6750  2ndnpr  6751  f1stres  6768  f2ndres  6769  1st2val  6772  2nd2val  6773  frxp  6856  soxp  6859  tz7.49  7112  elixpsn  7511  domdifsn  7603  domunsncan  7620  fineqvlem  7734  unblem4  7774  funsnfsupp  7855  ordiso2  7978  domwdom  8037  inf3lem3  8083  trcl  8159  unir1  8231  ssrankr1  8253  pm54.43lem  8380  infxpenlem  8391  ween  8412  acni3  8424  kmlem1  8526  infdif  8585  ackbij1lem1  8596  fin23lem14  8709  fin23lem32  8720  fin23lem40  8727  isfin1-3  8762  axcc2lem  8812  axdc3lem2  8827  axcclem  8833  ac6c4  8857  zornn0g  8881  axdclem2  8896  brdom3  8902  brdom5  8903  brdom4  8904  brdom6disj  8906  konigthlem  8939  pwcfsdom  8954  cfpwsdom  8955  alephom  8956  gruina  9189  grur1  9191  grothomex  9200  grothac  9201  nqpr  9385  axcnre  9534  axpre-sup  9539  ssxr  9649  le2tri3i  9710  0nn0  10830  uzind4  11163  rpnnen1lem5  11240  elfz4  11739  eluzfz  11741  ssfzo12bi  11951  hashgt0elex  12523  hashxplem  12548  hashfun  12552  ishashinf  12569  ffz0iswrd  12637  wrdsymb1  12647  ccatfv0  12671  lswccats1fst  12709  ccatswrd  12753  repswfsts  12825  cshw1  12862  swrdco  12875  cotr2g  12979  xptrrel  12983  trclun  13017  resqrex  13253  fsumsplitsnun  13754  ndvdsadd  14327  gcdcllem1  14411  gcdcllem3  14413  lcmftp  14547  lcmfunsnlem2lem2  14550  lcmfunsnlem2  14551  lcmfun  14556  1idssfct  14568  ncoprmgcdne1b  14593  coprmprod  14616  coprmproddvdslem  14617  prmodvdslcmf  14943  prmordvdslcmfOLD  14957  prmordvdslcmsOLDOLD  14959  cshwrepswhash1  15011  xpsff1o  15412  initoeu2  15849  clatlem  16295  clatlubcl2  16297  clatglbcl2  16299  xpsmnd  16514  sgrp2rid2  16598  xpsgrp  16743  symg2bas  16977  symgextf  16996  gsmsymgrfix  17007  gsmsymgreqlem2  17010  pmtr3ncom  17054  odlem1  17119  odlem1OLD  17122  gexlem1  17166  gexlem1OLD  17168  dprdfeq0  17593  gsumdixp  17775  lspcl  18137  cply1mul  18825  psgndiflemB  19105  lindfind  19311  lindsind  19312  lindsind2  19314  lindff1  19315  f1linds  19320  gsumcom3fi  19362  mat1dimscm  19437  dmatmul  19459  mdetdiag  19561  mdetunilem7  19580  mdetunilem9  19582  madurid  19606  fvmptnn04if  19810  tgcl  19922  elcls  20026  opnnei  20073  neiptopnei  20085  cnpnei  20217  cmpcov2  20342  cmpfii  20361  txcnp  20572  xpstps  20762  fbun  20792  isfild  20810  snfil  20816  filcon  20835  isufil2  20860  hauspwpwf1  20939  cnextcn  21019  ustfilxp  21164  ustuqtop4  21196  xpsxms  21486  xpsms  21487  rlmnvc  21642  nmoid  21700  xrsmopn  21767  xrhmeo  21911  cphsqrtcl  22099  iscmet3  22200  rrxcph  22288  iundisj  22438  ioorinv  22465  ioorinvOLD  22470  plyexmo  23203  aalioulem3  23227  dvtaylp  23262  dvradcnv  23313  logtayllem  23541  logtayl  23542  logbid1  23642  logbchbase  23645  relogbcxpb  23661  logbmpt  23662  logbfval  23664  musum  24057  pntlem3  24384  usgrarnedg  25048  nb3grapr  25118  nb3grapr2  25119  nb3gra2nb  25120  nbcusgra  25128  wlkcpr  25194  2pthlem2  25263  nvnencycllem  25308  wlkiswwlk2lem1  25356  clwwlkel  25458  clwwlkf1  25461  clwlkf1clwwlklem  25514  2wlkonotv  25542  clwlknclwlkdifs  25625  frgra0v  25658  frgra3v  25667  2pthfrgrarn  25674  2pthfrgra  25676  n4cyclfrgra  25683  frgrancvvdeqlem9  25706  frgrawopreglem3  25711  frgraregorufr0  25717  numclwwlk2lem1  25767  subgoablo  25976  ismndo2  26010  rngomndo  26086  sspval  26299  blo3i  26380  ajfval  26387  spanval  26923  cmcmlem  27181  cnvbraval  27700  leopnmid  27728  csmdsymi  27924  chirredlem4  27983  sumdmdlem  28008  ceqsexv2d  28071  iundisjf  28140  rnct  28245  padct  28252  xrge0infssOLD  28286  iundisjfi  28317  xrpxdivcld  28350  pnfneige0  28704  rrhre  28772  esumcocn  28848  hasheuni  28853  sgon  28893  sigapildsys  28931  ddemeas  29006  1stmbfm  29029  2ndmbfm  29030  dya2iocct  29049  dya2iocnrect  29050  eulerpartgbij  29152  eulerpartlemgs2  29160  coinflippv  29263  bnj1136  29753  bnj1175  29760  bnj1408  29792  cvmsdisj  29940  mrsubvrs  30107  mppspstlem  30156  problem4  30247  climuzcnv  30262  dfon2lem3  30377  dfon2lem7  30381  sltval2  30489  nodenselem5  30518  imageval  30641  filnetlem2  30979  df3nandALT1  31001  lukshef-ax2  31019  arg-ax  31020  sylbbr  31070  sylbb1  31071  sylbb2  31072  sylancl3  31107  bj-andnotim  31115  bj-modalbe  31182  bj-2uplex  31527  f1omptsnlem  31645  mptsnunlem  31647  onsucuni3  31677  finixpnum  31837  fin2solem  31838  poimirlem6  31853  poimirlem7  31854  poimirlem8  31855  poimirlem18  31865  poimirlem21  31868  poimirlem22  31869  poimirlem32  31879  mblfinlem3  31886  itg2addnclem2  31901  itg2addnc  31903  bddiblnc  31919  ftc1anclem6  31929  heiborlem3  32052  isfld2  32145  igenval2  32206  isfldidl  32208  dmncan2  32217  oprabbi  32312  mpt2bi123f  32313  opabbi  32316  ac6s3f  32321  lsat0cv  32511  pclfinclN  33427  docavalN  34603  djavalN  34615  dochval  34831  djhval  34878  dochexmidlem8  34947  dochkr1  34958  dochkr1OLDN  34959  hdmap1fval  35277  pellexlem5  35590  rmyabs  35721  jm2.24  35726  islssfgi  35843  pwslnm  35865  dgraaub  35926  dgraaubOLD  35927  clrellem  36142  frege114d  36263  frege55lem1a  36375  frege70  36442  3impexpbicom  36747  ee3bir  36772  vk15.4j  36798  onfrALTlem2  36825  ax6e2nd  36838  dfvd1impr  36860  dfvd2impr  36897  e1bir  36923  e2bir  36926  e3bir  37042  suctrALT  37138  19.21a3con13vVD  37164  3impexpbicomVD  37169  tratrbVD  37174  ssralv2VD  37179  truniALTVD  37191  trintALTVD  37193  undif3VD  37195  onfrALTlem3VD  37200  onfrALTlem2VD  37202  onfrALTVD  37204  relopabVD  37214  ax6e2ndVD  37221  2uasbanhVD  37224  vk15.4jVD  37227  sspwimp  37231  sspwimpVD  37232  sspwimpcf  37233  sspwimpcfVD  37234  suctrALTcf  37235  suctrALTcfVD  37236  suctrALT3  37237  sspwimpALT  37238  unisnALT  37239  ax6e2ndALT  37243  isosctrlem1ALT  37247  iunconlem2  37248  infrglbOLD  37552  cncfuni  37647  iblcncfioo  37738  stoweidlem14  37757  stoweidlem17  37760  stoweidlem35  37779  stoweidlem57  37801  stirlinglem7  37825  stirlinglem10  37828  fourierdlem54  37907  fourierdlem62  37915  fourierdlem63  37916  fourierdlem65  37918  fourierdlem73  37926  fourierdlem80  37933  fourierdlem82  37935  fourierdlem101  37954  etransclem32  38014  meadjiunlem  38154  ismeannd  38156  caratheodory  38200  ovnsubaddlem2  38240  hoidmvlelem5  38268  aibandbiaiaiffb  38296  fnresfnco  38441  dfdfat2  38446  afvres  38487  tz6.12-afv  38488  ndmaovass  38521  el1fzopredsuc  38535  iccpartiltu  38549  iccelpart  38560  evenprm2  38655  lswn0  38733  ccatpfx  38763  2f1fvneq  38820  fzoopth  38860  upgredg  38990  umgredg  38991  nbupgrel  39149  nb3gr2nb  39189  cplgruvtxb  39211  spthdifv  39257  lincext1  39840