Theorem biimpri 198

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 194	. 2 |- ( ps <-> ph )
3	2	biimpi 187	1 |- ( ps -> ph )

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

This theorem is referenced by:  mpbir  201  sylibr  204  sylbir  205  syl5bir  210  syl6ibr  219  bitri  241  mtbi  290  pm2.54  364  sylanbr  460  sylan2br  463  pm3.11  486  orbi2i  506  pm2.31  512  simplbi2  609  dfbi  611  pm2.85  827  rnlem  932  syl3an1br  1223  syl3an2br  1224  syl3an3br  1225  3impexpbicom  1373  nic-axALT  1445  sbbii  1661  hbn1fw  1715  hbn1fwOLD  1716  equveliOLD  2043  exmoeu  2296  eueq2  3068  ralun  3489  ssunieq  4008  ax9vsep  4294  ordunidif  4589  unizlim  4657  dfwe2  4721  onminex  4746  nnsuc  4821  opelxpi  4869  ndmima  5200  funtpg  5460  dffo2  5616  dff1o2  5638  resdif  5655  f1o00  5669  fvimacnvALT  5808  exfo  5846  ressnop0  5872  fsnunfv  5892  ovid  6149  ovidig  6150  f1stres  6327  f2ndres  6328  1st2val  6331  2nd2val  6332  frxp  6415  soxp  6418  tz7.49  6661  abianfp  6675  elixpsn  7060  domdifsn  7150  domunsncan  7167  fineqvlem  7282  unblem4  7321  ordiso2  7440  domwdom  7498  inf3lem3  7541  trcl  7620  unir1  7695  ssrankr1  7717  pm54.43lem  7842  infxpenlem  7851  ween  7872  acni3  7884  kmlem1  7986  infdif  8045  ackbij1lem1  8056  fin23lem14  8169  fin23lem32  8180  fin23lem40  8187  isfin1-3  8222  axcc2lem  8272  axdc3lem2  8287  axcclem  8293  ac6c4  8317  zornn0g  8341  axdclem2  8356  brdom3  8362  brdom5  8363  brdom4  8364  brdom6disj  8366  konigthlem  8399  pwcfsdom  8414  cfpwsdom  8415  alephom  8416  gruina  8649  grur1  8651  grothomex  8660  grothac  8661  nqpr  8847  axcnre  8995  axpre-sup  9000  ssxr  9101  le2tri3i  9159  0nn0  10192  uzind4  10490  rpnnen1lem5  10560  elfz4  11008  eluzfz  11010  hashgt0elex  11625  hashxplem  11651  hashfun  11655  ccatswrd  11728  resqrex  12011  ndvdsadd  12883  gcdcllem1  12966  gcdcllem3  12968  1idssfct  13040  xpsff1o  13748  xpsmnd  14690  xpsgrp  14892  odlem1  15128  gexlem1  15168  dprdfeq0  15535  gsumdixp  15670  lspcl  16007  tgcl  16989  elcls  17092  opnnei  17139  neiptopnei  17151  cnpnei  17282  cmpcov2  17407  cmpfii  17426  txcnp  17605  xpstps  17795  fbun  17825  isfild  17843  snfil  17849  filcon  17868  isufil2  17893  hauspwpwf1  17972  cnextcn  18051  ustfilxp  18195  ustuqtop4  18227  xpsxms  18517  xpsms  18518  rlmnvc  18691  nmoid  18729  xrsmopn  18796  xrhmeo  18924  cphsqrcl  19100  iscmet3  19199  iundisj  19395  ioorinv  19421  plyexmo  20183  aalioulem3  20204  dvtaylp  20239  dvradcnv  20290  logtayllem  20503  logtayl  20504  musum  20929  pntlem3  21256  usgrarnedg  21357  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  nbcusgra  21425  2pthlem2  21549  nvnencycllem  21583  subgoablo  21852  ismndo2  21886  rngomndo  21962  sspval  22175  blo3i  22256  ajfval  22263  spanval  22788  cmcmlem  23046  cnvbraval  23566  leopnmid  23594  csmdsymi  23790  chirredlem4  23849  sumdmdlem  23874  ceqsexv2d  23938  iundisjf  23982  1stnpr  24046  2ndnpr  24047  rnct  24061  iundisjfi  24105  ishashinf  24112  xrpxdivcld  24134  pnfneige0  24289  rrhre  24340  logbid1  24351  esumcocn  24423  hasheuni  24428  sgon  24460  1stmbfm  24563  2ndmbfm  24564  dya2iocct  24583  dya2iocnrect  24584  sibfof  24607  coinflippv  24694  cvmsdisj  24910  climuzcnv  25061  dfon2lem3  25355  dfon2lem7  25359  sspred  25388  sltval2  25524  nodenselem5  25553  imageval  25683  df3nandALT1  26050  lukshef-ax2  26069  arg-ax  26070  mblfinlem2  26144  itg2addnclem2  26156  itg2addnc  26158  bddiblnc  26174  filnetlem2  26298  heiborlem3  26412  isfld2  26505  igenval2  26566  isfldidl  26568  dmncan2  26577  pellexlem5  26786  rmyabs  26913  jm2.24  26918  islssfgi  27038  pwslnm  27064  lindfind  27154  lindsind  27155  lindsind2  27157  lindff1  27158  f1linds  27163  islindf4  27176  dgraaub  27221  gsumcom3fi  27323  infrglb  27589  stoweidlem14  27630  stoweidlem17  27633  stoweidlem35  27651  stoweidlem55  27671  stoweidlem57  27673  stoweid  27679  stirlinglem7  27696  stirlinglem10  27699  aibandbiaiaiffb  27730  fnresfnco  27857  dfdfat2  27862  afvres  27903  tz6.12-afv  27904  ndmaovass  27937  2f1fvneq  27958  swrdccatin2  28018  spthdifv  28039  2wlkonotv  28074  frgra0v  28097  frgra3v  28106  2pthfrgrarn  28113  2pthfrgra  28115  n4cyclfrgra  28122  frgrancvvdeqlem9  28144  frgrawopreglem3  28149  frgraregorufr0  28155  ee3bir  28296  vk15.4j  28323  onfrALTlem2  28343  a9e2nd  28356  dfvd1impr  28377  dfvd2impr  28414  e1bir  28440  e2bir  28443  e3bir  28560  19.21a3con13vVD  28673  3impexpbicomVD  28678  tratrbVD  28682  ssralv2VD  28687  truniALTVD  28699  trintALTVD  28701  undif3VD  28703  onfrALTlem3VD  28708  onfrALTlem2VD  28710  onfrALTVD  28712  relopabVD  28722  a9e2ndVD  28729  2uasbanhVD  28732  vk15.4jVD  28735  sspwimp  28739  sspwimpVD  28740  sspwimpcf  28741  sspwimpcfVD  28742  suctrALTcf  28743  suctrALTcfVD  28744  suctrALT3  28745  sspwimpALT  28746  unisnALT  28747  a9e2ndALT  28752  bnj1136  29072  bnj1175  29079  bnj1408  29111  equveliNEW7  29232  lsat0cv  29516  pclfinclN  30432  docavalN  31606  djavalN  31618  dochval  31834  djhval  31881  dochexmidlem8  31950  dochkr1  31961  dochkr1OLDN  31962  hdmap1fval  32280

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178