Theorem biimpri 211

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

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

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 190

This theorem is referenced by:  mpbir  214  sylibr  217  sylbir  218  sylbbr  219  sylbb1  220  sylbb2  221  syl5bir  226  syl6ibr  235  mtbi  304  pm2.54  380  sylanbr  480  sylan2br  483  pm3.11  506  orbi2i  526  pm2.31  532  simplbi2  635  dfbi  639  pm2.85  869  rnlemOLD  982  syl3an1br  1315  syl3an2br  1316  syl3an3br  1317  had1  1517  nic-axALT  1568  speimfw  1804  sbbii  1815  exmidne  2645  ceqsexv2d  3097  eueq2  3224  ralun  3628  euelss  3742  ssunieq  4246  ax6vsep  4543  opelxpi  4885  ndmima  5224  ndmimaOLD  5225  elsnxp  5397  sspred  5407  ordunidif  5490  unizlim  5558  funtpg  5651  dffo2  5820  dff1o2  5842  resdif  5857  f1o00  5870  fvimacnvALT  6024  fvcofneq  6053  exfo  6063  ressnop0  6095  fsnunfv  6128  ovid  6440  ovidig  6441  dfwe2  6635  onminex  6661  nnsuc  6736  1stnpr  6824  2ndnpr  6825  f1stres  6842  f2ndres  6843  1st2val  6846  2nd2val  6847  frxp  6933  soxp  6936  tz7.49  7188  elixpsn  7587  domdifsn  7681  domunsncan  7698  fineqvlem  7812  unblem4  7852  funsnfsupp  7933  ordiso2  8056  domwdom  8115  inf3lem3  8161  trcl  8238  unir1  8310  ssrankr1  8332  pm54.43lem  8459  infxpenlem  8470  ween  8492  acni3  8504  kmlem1  8606  infdif  8665  ackbij1lem1  8676  fin23lem14  8789  fin23lem32  8800  fin23lem40  8807  isfin1-3  8842  axcc2lem  8892  axdc3lem2  8907  axcclem  8913  ac6c4  8937  zornn0g  8961  axdclem2  8976  brdom3  8982  brdom5  8983  brdom4  8984  brdom6disj  8986  konigthlem  9019  pwcfsdom  9034  cfpwsdom  9035  alephom  9036  gruina  9269  grur1  9271  grothomex  9280  grothac  9281  nqpr  9465  axcnre  9614  axpre-sup  9619  ssxr  9729  le2tri3i  9790  0nn0  10913  uzind4  11246  rpnnen1lem5  11323  elfz4  11822  eluzfz  11824  ssfzo12bi  12037  hashgt0elex  12610  hashxplem  12638  hashfun  12642  ishashinf  12659  ffz0iswrd  12730  wrdsymb1  12740  ccatfv0  12764  lswccats1fst  12805  ccatswrd  12849  repswfsts  12921  cshw1  12958  swrdco  12971  cotr2g  13089  xptrrel  13093  trclun  13127  resqrex  13363  fsumsplitsnun  13865  ndvdsadd  14438  gcdcllem1  14522  gcdcllem3  14524  lcmftp  14658  lcmfunsnlem2lem2  14661  lcmfunsnlem2  14662  lcmfun  14667  1idssfct  14679  ncoprmgcdne1b  14704  coprmprod  14727  coprmproddvdslem  14728  prmodvdslcmf  15054  prmordvdslcmfOLD  15068  prmordvdslcmsOLDOLD  15070  cshwrepswhash1  15122  xpsff1o  15523  initoeu2  15960  clatlem  16406  clatlubcl2  16408  clatglbcl2  16410  xpsmnd  16625  sgrp2rid2  16709  xpsgrp  16854  symg2bas  17088  symgextf  17107  gsmsymgrfix  17118  gsmsymgreqlem2  17121  pmtr3ncom  17165  odlem1  17230  odlem1OLD  17233  gexlem1  17277  gexlem1OLD  17279  dprdfeq0  17704  gsumdixp  17886  lspcl  18248  cply1mul  18936  psgndiflemB  19217  lindfind  19423  lindsind  19424  lindsind2  19426  lindff1  19427  f1linds  19432  gsumcom3fi  19474  mat1dimscm  19549  dmatmul  19571  mdetdiag  19673  mdetunilem7  19692  mdetunilem9  19694  madurid  19718  fvmptnn04if  19922  tgcl  20034  elcls  20138  opnnei  20185  neiptopnei  20197  cnpnei  20329  cmpcov2  20454  cmpfii  20473  txcnp  20684  xpstps  20874  fbun  20904  isfild  20922  snfil  20928  filcon  20947  isufil2  20972  hauspwpwf1  21051  cnextcn  21131  ustfilxp  21276  ustuqtop4  21308  xpsxms  21598  xpsms  21599  rlmnvc  21754  nmoid  21812  xrsmopn  21879  xrhmeo  22023  cphsqrtcl  22211  iscmet3  22312  rrxcph  22400  iundisj  22550  ioorinv  22577  ioorinvOLD  22582  plyexmo  23315  aalioulem3  23339  dvtaylp  23374  dvradcnv  23425  logtayllem  23653  logtayl  23654  logbid1  23754  logbchbase  23757  relogbcxpb  23773  logbmpt  23774  logbfval  23776  musum  24169  pntlem3  24496  usgrarnedg  25160  nb3grapr  25230  nb3grapr2  25231  nb3gra2nb  25232  nbcusgra  25240  wlkcpr  25306  2pthlem2  25375  nvnencycllem  25420  wlkiswwlk2lem1  25468  clwwlkel  25570  clwwlkf1  25573  clwlkf1clwwlklem  25626  2wlkonotv  25654  clwlknclwlkdifs  25737  frgra0v  25770  frgra3v  25779  2pthfrgrarn  25786  2pthfrgra  25788  n4cyclfrgra  25795  frgrancvvdeqlem9  25818  frgrawopreglem3  25823  frgraregorufr0  25829  numclwwlk2lem1  25879  subgoablo  26088  ismndo2  26122  rngomndo  26198  sspval  26411  blo3i  26492  ajfval  26499  spanval  27035  cmcmlem  27293  cnvbraval  27812  leopnmid  27840  csmdsymi  28036  chirredlem4  28095  sumdmdlem  28120  iundisjf  28248  rnct  28349  padct  28356  xrge0infssOLD  28390  iundisjfi  28421  xrpxdivcld  28453  pnfneige0  28806  rrhre  28874  esumcocn  28950  hasheuni  28955  sgon  28995  sigapildsys  29033  ddemeas  29108  1stmbfm  29131  2ndmbfm  29132  dya2iocct  29151  dya2iocnrect  29152  eulerpartgbij  29254  eulerpartlemgs2  29262  coinflippv  29365  bnj1136  29855  bnj1175  29862  bnj1408  29894  cvmsdisj  30042  mrsubvrs  30209  mppspstlem  30258  problem4  30349  climuzcnv  30364  dfon2lem3  30480  dfon2lem7  30484  sltval2  30592  nodenselem5  30623  imageval  30746  filnetlem2  31084  df3nandALT1  31106  lukshef-ax2  31124  arg-ax  31125  sylancl3  31209  bj-andnotim  31217  bj-modalbe  31326  bj-2uplex  31661  f1omptsnlem  31783  mptsnunlem  31785  onsucuni3  31815  finixpnum  31975  fin2solem  31976  poimirlem6  31991  poimirlem7  31992  poimirlem8  31993  poimirlem18  32003  poimirlem21  32006  poimirlem22  32007  poimirlem32  32017  mblfinlem3  32024  itg2addnclem2  32039  itg2addnc  32041  bddiblnc  32057  ftc1anclem6  32067  heiborlem3  32190  isfld2  32283  igenval2  32344  isfldidl  32346  dmncan2  32355  oprabbi  32450  mpt2bi123f  32451  opabbi  32454  ac6s3f  32459  lsat0cv  32644  pclfinclN  33560  docavalN  34736  djavalN  34748  dochval  34964  djhval  35011  dochexmidlem8  35080  dochkr1  35091  dochkr1OLDN  35092  hdmap1fval  35410  pellexlem5  35722  rmyabs  35853  jm2.24  35858  islssfgi  35975  pwslnm  35997  dgraaub  36058  dgraaubOLD  36059  clrellem  36274  frege114d  36395  frege55lem1a  36507  frege70  36574  3impexpbicom  36878  ee3bir  36903  vk15.4j  36929  onfrALTlem2  36956  ax6e2nd  36969  dfvd1impr  36989  dfvd2impr  37026  e1bir  37052  e2bir  37055  e3bir  37166  suctrALT  37262  19.21a3con13vVD  37288  3impexpbicomVD  37293  tratrbVD  37298  ssralv2VD  37303  truniALTVD  37315  trintALTVD  37317  undif3VD  37319  onfrALTlem3VD  37324  onfrALTlem2VD  37326  onfrALTVD  37328  relopabVD  37338  ax6e2ndVD  37345  2uasbanhVD  37348  vk15.4jVD  37351  sspwimp  37355  sspwimpVD  37356  sspwimpcf  37357  sspwimpcfVD  37358  suctrALTcf  37359  suctrALTcfVD  37360  suctrALT3  37361  sspwimpALT  37362  unisnALT  37363  ax6e2ndALT  37367  isosctrlem1ALT  37371  iunconlem2  37372  infrglbOLD  37707  cncfuni  37802  iblcncfioo  37893  stoweidlem14  37912  stoweidlem17  37915  stoweidlem35  37934  stoweidlem57  37956  stirlinglem7  37980  stirlinglem10  37983  fourierdlem54  38062  fourierdlem62  38070  fourierdlem63  38071  fourierdlem65  38073  fourierdlem73  38081  fourierdlem80  38088  fourierdlem82  38090  fourierdlem101  38109  etransclem32  38169  meadjiunlem  38341  ismeannd  38343  caratheodory  38387  ovnsubaddlem2  38431  hoidmvlelem5  38459  hoiqssbllem2  38483  aibandbiaiaiffb  38520  fnresfnco  38665  dfdfat2  38671  afvres  38712  tz6.12-afv  38713  ndmaovass  38746  el1fzopredsuc  38760  iccpartiltu  38774  iccelpart  38785  evenprm2  38880  lswn0  38960  ccatpfx  38990  2f1fvneq  39054  fzoopth  39105  upgredg  39276  umgredg  39277  nbupgrel  39463  nbusgrvtxm1  39503  nb3gr2nb  39508  cplgruvtxb  39533  pthdivtx  39762  pthdlem2lem  39793  umgr3v3e3cycl  39925  spthdifv  39939  lincext1  40520