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  1501  nic-axALT  1553  speimfw  1785  sbbii  1796  exmidne  2636  eueq2  3251  ralun  3654  euelss  3766  ssunieq  4256  ax6vsep  4552  opelxpi  4886  ndmima  5225  ndmimaOLD  5226  sspred  5407  ordunidif  5490  unizlim  5558  funtpg  5651  dffo2  5814  dff1o2  5836  resdif  5851  f1o00  5863  fvimacnvALT  6016  fvcofneq  6045  exfo  6055  ressnop0  6086  fsnunfv  6119  ovid  6427  ovidig  6428  dfwe2  6622  onminex  6648  nnsuc  6723  1stnpr  6811  2ndnpr  6812  f1stres  6829  f2ndres  6830  1st2val  6833  2nd2val  6834  frxp  6917  soxp  6920  tz7.49  7170  elixpsn  7569  domdifsn  7661  domunsncan  7678  fineqvlem  7792  unblem4  7832  funsnfsupp  7913  ordiso2  8030  domwdom  8089  inf3lem3  8135  trcl  8211  unir1  8283  ssrankr1  8305  pm54.43lem  8432  infxpenlem  8443  ween  8464  acni3  8476  kmlem1  8578  infdif  8637  ackbij1lem1  8648  fin23lem14  8761  fin23lem32  8772  fin23lem40  8779  isfin1-3  8814  axcc2lem  8864  axdc3lem2  8879  axcclem  8885  ac6c4  8909  zornn0g  8933  axdclem2  8948  brdom3  8954  brdom5  8955  brdom4  8956  brdom6disj  8958  konigthlem  8991  pwcfsdom  9006  cfpwsdom  9007  alephom  9008  gruina  9242  grur1  9244  grothomex  9253  grothac  9254  nqpr  9438  axcnre  9587  axpre-sup  9592  ssxr  9702  le2tri3i  9763  0nn0  10884  uzind4  11217  rpnnen1lem5  11294  elfz4  11791  eluzfz  11793  ssfzo12bi  12003  hashgt0elex  12575  hashxplem  12600  hashfun  12604  ffz0iswrd  12681  wrdsymb1  12691  ccatfv0  12715  lswccats1fst  12753  ccatswrd  12797  repswfsts  12869  cshw1  12906  swrdco  12919  cotr2g  13019  xptrrel  13023  trclun  13057  resqrex  13293  fsumsplitsnun  13794  ndvdsadd  14364  gcdcllem1  14447  gcdcllem3  14449  lcmftp  14571  lcmfunsnlem2lem2  14574  lcmfunsnlem2  14575  lcmfun  14580  1idssfct  14592  ncoprmgcdne1b  14617  coprmprod  14640  coprmproddvdslem  14641  prmodvdslcmf  14959  prmordvdslcmfOLD  14973  prmordvdslcmsOLDOLD  14975  cshwrepswhash1  15027  xpsff1o  15416  initoeu2  15853  clatlem  16299  clatlubcl2  16301  clatglbcl2  16303  xpsmnd  16518  sgrp2rid2  16602  xpsgrp  16747  symg2bas  16981  symgextf  17000  gsmsymgrfix  17011  gsmsymgreqlem2  17014  pmtr3ncom  17058  odlem1  17117  gexlem1  17157  dprdfeq0  17581  gsumdixp  17763  lspcl  18125  cply1mul  18813  psgndiflemB  19090  lindfind  19296  lindsind  19297  lindsind2  19299  lindff1  19300  f1linds  19305  gsumcom3fi  19347  mat1dimscm  19422  dmatmul  19444  mdetdiag  19546  mdetunilem7  19565  mdetunilem9  19567  madurid  19591  fvmptnn04if  19795  tgcl  19907  elcls  20011  opnnei  20058  neiptopnei  20070  cnpnei  20202  cmpcov2  20327  cmpfii  20346  txcnp  20557  xpstps  20747  fbun  20777  isfild  20795  snfil  20801  filcon  20820  isufil2  20845  hauspwpwf1  20924  cnextcn  21004  ustfilxp  21149  ustuqtop4  21181  xpsxms  21471  xpsms  21472  rlmnvc  21627  nmoid  21665  xrsmopn  21732  xrhmeo  21861  cphsqrtcl  22046  iscmet3  22147  rrxcph  22235  iundisj  22369  ioorinv  22396  ioorinvOLD  22401  plyexmo  23125  aalioulem3  23146  dvtaylp  23181  dvradcnv  23232  logtayllem  23460  logtayl  23461  logbid1  23561  logbchbase  23564  relogbcxpb  23580  logbmpt  23581  logbfval  23583  musum  23974  pntlem3  24301  usgrarnedg  24948  nb3grapr  25017  nb3grapr2  25018  nb3gra2nb  25019  nbcusgra  25027  wlkcpr  25093  2pthlem2  25162  nvnencycllem  25207  wlkiswwlk2lem1  25255  clwwlkel  25357  clwwlkf1  25360  clwlkf1clwwlklem  25413  2wlkonotv  25441  clwlknclwlkdifs  25524  frgra0v  25557  frgra3v  25566  2pthfrgrarn  25573  2pthfrgra  25575  n4cyclfrgra  25582  frgrancvvdeqlem9  25605  frgrawopreglem3  25610  frgraregorufr0  25616  numclwwlk2lem1  25666  subgoablo  25875  ismndo2  25909  rngomndo  25985  sspval  26198  blo3i  26279  ajfval  26286  spanval  26812  cmcmlem  27070  cnvbraval  27589  leopnmid  27617  csmdsymi  27813  chirredlem4  27872  sumdmdlem  27897  ceqsexv2d  27960  iundisjf  28029  elsnxp  28054  rnct  28134  padct  28141  xrge0infss  28172  iundisjfi  28199  ishashinf  28208  xrpxdivcld  28233  pnfneige0  28587  rrhre  28655  esumcocn  28731  hasheuni  28736  sgon  28776  sigapildsys  28814  ddemeas  28889  1stmbfm  28912  2ndmbfm  28913  dya2iocct  28932  dya2iocnrect  28933  eulerpartgbij  29022  eulerpartlemgs2  29030  coinflippv  29133  bnj1136  29585  bnj1175  29592  bnj1408  29624  cvmsdisj  29772  mrsubvrs  29939  mppspstlem  29988  problem4  30079  climuzcnv  30094  dfon2lem3  30209  dfon2lem7  30213  sltval2  30321  nodenselem5  30350  imageval  30473  filnetlem2  30811  df3nandALT1  30833  lukshef-ax2  30851  arg-ax  30852  sylbbr  30902  sylbb1  30903  sylbb2  30904  sylancl3  30939  bj-andnotim  30947  bj-modalbe  31012  bj-2uplex  31356  f1omptsnlem  31463  mptsnunlem  31465  finixpnum  31624  fin2solem  31625  poimirlem6  31640  poimirlem7  31641  poimirlem8  31642  poimirlem18  31652  poimirlem21  31655  poimirlem22  31656  poimirlem32  31666  mblfinlem3  31673  itg2addnclem2  31688  itg2addnc  31690  bddiblnc  31706  ftc1anclem6  31716  heiborlem3  31839  isfld2  31932  igenval2  31993  isfldidl  31995  dmncan2  32004  oprabbi  32099  mpt2bi123f  32100  opabbi  32103  ac6s3f  32108  lsat0cv  32298  pclfinclN  33214  docavalN  34390  djavalN  34402  dochval  34618  djhval  34665  dochexmidlem8  34734  dochkr1  34745  dochkr1OLDN  34746  hdmap1fval  35064  pellexlem5  35377  rmyabs  35504  jm2.24  35509  islssfgi  35626  pwslnm  35648  dgraaub  35703  frege114d  35979  frege55lem1a  36089  frege70  36156  3impexpbicom  36461  ee3bir  36486  vk15.4j  36512  onfrALTlem2  36539  ax6e2nd  36552  dfvd1impr  36574  dfvd2impr  36611  e1bir  36637  e2bir  36640  e3bir  36756  suctrALT  36852  19.21a3con13vVD  36878  3impexpbicomVD  36883  tratrbVD  36888  ssralv2VD  36893  truniALTVD  36905  trintALTVD  36907  undif3VD  36909  onfrALTlem3VD  36914  onfrALTlem2VD  36916  onfrALTVD  36918  relopabVD  36928  ax6e2ndVD  36935  2uasbanhVD  36938  vk15.4jVD  36941  sspwimp  36945  sspwimpVD  36946  sspwimpcf  36947  sspwimpcfVD  36948  suctrALTcf  36949  suctrALTcfVD  36950  suctrALT3  36951  sspwimpALT  36952  unisnALT  36953  ax6e2ndALT  36957  isosctrlem1ALT  36961  iunconlem2  36962  infrglbOLD  37231  cncfuni  37326  iblcncfioo  37414  stoweidlem14  37433  stoweidlem17  37436  stoweidlem35  37455  stoweidlem57  37477  stirlinglem7  37501  stirlinglem10  37504  fourierdlem54  37582  fourierdlem62  37590  fourierdlem63  37591  fourierdlem65  37593  fourierdlem73  37601  fourierdlem80  37608  fourierdlem82  37610  fourierdlem101  37629  etransclem32  37688  meadjiunlem  37802  ismeannd  37804  caratheodory  37848  aibandbiaiaiffb  37872  fnresfnco  38008  dfdfat2  38013  afvres  38054  tz6.12-afv  38055  ndmaovass  38088  el1fzopredsuc  38102  iccpartiltu  38116  iccelpart  38127  evenprm2  38222  lswn0  38300  ccatpfx  38330  2f1fvneq  38374  fzoopth  38402  spthdifv  38412  lincext1  38997