MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpri Structured version   Unicode version

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
StepHypRef Expression
1 biimpri.1 . . 3  |-  ( ph  <->  ps )
21bicomi 194 . 2  |-  ( ps  <->  ph )
32biimpi 187 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
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  1376  nic-axALT  1448  sbbii  1665  hbn1fw  1719  hbn1fwOLD  1720  equveliOLD  2082  exmoeu  2322  eueq2  3100  ralun  3521  ssunieq  4040  ax9vsep  4326  ordunidif  4621  suctr  4657  unizlim  4690  dfwe2  4754  onminex  4779  nnsuc  4854  opelxpi  4902  ndmima  5233  funtpg  5493  dffo2  5649  dff1o2  5671  resdif  5688  f1o00  5702  fvimacnvALT  5841  exfo  5879  ressnop0  5905  fsnunfv  5925  ovid  6182  ovidig  6183  f1stres  6360  f2ndres  6361  1st2val  6364  2nd2val  6365  frxp  6448  soxp  6451  tz7.49  6694  abianfp  6708  elixpsn  7093  domdifsn  7183  domunsncan  7200  fineqvlem  7315  unblem4  7354  ordiso2  7474  domwdom  7532  inf3lem3  7575  trcl  7654  unir1  7729  ssrankr1  7751  pm54.43lem  7876  infxpenlem  7885  ween  7906  acni3  7918  kmlem1  8020  infdif  8079  ackbij1lem1  8090  fin23lem14  8203  fin23lem32  8214  fin23lem40  8221  isfin1-3  8256  axcc2lem  8306  axdc3lem2  8321  axcclem  8327  ac6c4  8351  zornn0g  8375  axdclem2  8390  brdom3  8396  brdom5  8397  brdom4  8398  brdom6disj  8400  konigthlem  8433  pwcfsdom  8448  cfpwsdom  8449  alephom  8450  gruina  8683  grur1  8685  grothomex  8694  grothac  8695  nqpr  8881  axcnre  9029  axpre-sup  9034  ssxr  9135  le2tri3i  9193  0nn0  10226  uzind4  10524  rpnnen1lem5  10594  elfz4  11042  eluzfz  11044  hashgt0elex  11660  hashxplem  11686  hashfun  11690  ccatswrd  11763  resqrex  12046  ndvdsadd  12918  gcdcllem1  13001  gcdcllem3  13003  1idssfct  13075  xpsff1o  13783  xpsmnd  14725  xpsgrp  14927  odlem1  15163  gexlem1  15203  dprdfeq0  15570  gsumdixp  15705  lspcl  16042  tgcl  17024  elcls  17127  opnnei  17174  neiptopnei  17186  cnpnei  17318  cmpcov2  17443  cmpfii  17462  txcnp  17642  xpstps  17832  fbun  17862  isfild  17880  snfil  17886  filcon  17905  isufil2  17930  hauspwpwf1  18009  cnextcn  18088  ustfilxp  18232  ustuqtop4  18264  xpsxms  18554  xpsms  18555  rlmnvc  18728  nmoid  18766  xrsmopn  18833  xrhmeo  18961  cphsqrcl  19137  iscmet3  19236  iundisj  19432  ioorinv  19458  plyexmo  20220  aalioulem3  20241  dvtaylp  20276  dvradcnv  20327  logtayllem  20540  logtayl  20541  musum  20966  pntlem3  21293  usgrarnedg  21394  nb3grapr  21452  nb3grapr2  21453  nb3gra2nb  21454  nbcusgra  21462  2pthlem2  21586  nvnencycllem  21620  subgoablo  21889  ismndo2  21923  rngomndo  21999  sspval  22212  blo3i  22293  ajfval  22300  spanval  22825  cmcmlem  23083  cnvbraval  23603  leopnmid  23631  csmdsymi  23827  chirredlem4  23886  sumdmdlem  23911  ceqsexv2d  23975  iundisjf  24019  1stnpr  24083  2ndnpr  24084  rnct  24098  iundisjfi  24142  ishashinf  24149  xrpxdivcld  24171  pnfneige0  24326  rrhre  24377  logbid1  24388  esumcocn  24460  hasheuni  24465  sgon  24497  1stmbfm  24600  2ndmbfm  24601  dya2iocct  24620  dya2iocnrect  24621  sibfof  24644  coinflippv  24731  cvmsdisj  24947  climuzcnv  25098  dfon2lem3  25400  dfon2lem7  25404  sspred  25434  sltval2  25576  nodenselem5  25605  imageval  25740  df3nandALT1  26111  lukshef-ax2  26130  arg-ax  26131  mblfinlem2  26208  itg2addnclem2  26220  itg2addnc  26222  bddiblnc  26238  filnetlem2  26362  heiborlem3  26476  isfld2  26569  igenval2  26630  isfldidl  26632  dmncan2  26641  pellexlem5  26850  rmyabs  26977  jm2.24  26982  islssfgi  27102  pwslnm  27128  lindfind  27218  lindsind  27219  lindsind2  27221  lindff1  27222  f1linds  27227  islindf4  27240  dgraaub  27285  gsumcom3fi  27387  infrglb  27653  stoweidlem14  27694  stoweidlem17  27697  stoweidlem35  27715  stoweidlem55  27735  stoweidlem57  27737  stoweid  27743  stirlinglem7  27760  stirlinglem10  27763  aibandbiaiaiffb  27794  fnresfnco  27921  dfdfat2  27926  afvres  27967  tz6.12-afv  27968  ndmaovass  28001  2f1fvneq  28027  ccatsymb  28116  lswrdn0  28190  cshw1  28202  cshw1v  28203  cshwssizelem2  28208  spthdifv  28226  2wlkonotv  28261  frgra0v  28284  frgra3v  28293  2pthfrgrarn  28300  2pthfrgra  28302  n4cyclfrgra  28309  frgrancvvdeqlem9  28331  frgrawopreglem3  28336  frgraregorufr0  28342  ee3bir  28486  vk15.4j  28513  onfrALTlem2  28533  a9e2nd  28546  dfvd1impr  28569  dfvd2impr  28606  e1bir  28632  e2bir  28635  e3bir  28752  19.21a3con13vVD  28865  3impexpbicomVD  28870  tratrbVD  28874  ssralv2VD  28879  truniALTVD  28891  trintALTVD  28893  undif3VD  28895  onfrALTlem3VD  28900  onfrALTlem2VD  28902  onfrALTVD  28904  relopabVD  28914  a9e2ndVD  28921  2uasbanhVD  28924  vk15.4jVD  28927  sspwimp  28931  sspwimpVD  28932  sspwimpcf  28933  sspwimpcfVD  28934  suctrALTcf  28935  suctrALTcfVD  28936  suctrALT3  28937  sspwimpALT  28938  unisnALT  28939  a9e2ndALT  28943  isosctrlem1ALT  28947  iunconlem2  28948  bnj1136  29267  bnj1175  29274  bnj1408  29306  equveliNEW7  29429  ax7w10AUX7  29563  lsat0cv  29732  pclfinclN  30648  docavalN  31822  djavalN  31834  dochval  32050  djhval  32097  dochexmidlem8  32166  dochkr1  32177  dochkr1OLDN  32178  hdmap1fval  32496
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
  Copyright terms: Public domain W3C validator