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

Theorem biimpri 199
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 195 . 2  |-  ( ps  <->  ph )
32biimpi 188 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  mpbir  202  sylibr  205  sylbir  206  syl5bir  211  syl6ibr  220  bitri  242  mtbi  291  pm2.54  365  sylanbr  461  sylan2br  464  pm3.11  487  orbi2i  507  pm2.31  513  simplbi2  611  dfbi  613  pm2.85  829  pm3.43OLD  840  rnlem  936  syl3an1br  1226  syl3an2br  1227  syl3an3br  1228  3impexpbicom  1363  nic-axALT  1434  equveli  1881  sbbii  1886  exmoeu  2160  eueq2  2914  ralun  3332  ssunieq  3834  ax9vsep  4119  ordunidif  4412  unizlim  4481  dfwe2  4545  onminex  4570  nnsuc  4645  opelxpi  4709  ndmima  5038  dffo2  5393  dff1o2  5415  resdif  5432  f1o00  5446  fvimacnvALT  5578  exfo  5612  ressnop0  5637  fsnunfv  5654  ovid  5898  ovidig  5899  f1stres  6075  f2ndres  6076  1st2val  6079  2nd2val  6080  frxp  6159  soxp  6162  tz7.49  6425  abianfp  6439  elixpsn  6823  domdifsn  6913  domunsncan  6930  fineqvlem  7045  unblem4  7080  ordiso2  7198  domwdom  7256  inf3lem3  7299  trcl  7378  unir1  7453  ssrankr1  7475  pm54.43lem  7600  infxpenlem  7609  ween  7630  acni3  7642  kmlem1  7744  infdif  7803  ackbij1lem1  7814  fin23lem14  7927  fin23lem32  7938  fin23lem40  7945  isfin1-3  7980  axcc2lem  8030  axdc3lem2  8045  axcclem  8051  ac6c4  8076  zornn0g  8100  axdclem2  8115  brdom3  8121  brdom5  8122  brdom4  8123  brdom6disj  8125  konigthlem  8158  pwcfsdom  8173  cfpwsdom  8174  alephom  8175  gruina  8408  grur1  8410  grothomex  8419  grothac  8420  nqpr  8606  axcnre  8754  axpre-sup  8759  ssxr  8860  le2tri3i  8917  0nn0  9947  uzind4  10243  rpnnen1lem5  10313  elfz4  10757  eluzfz  10759  hashxplem  11350  hashfun  11354  ccatswrd  11424  resqrex  11701  ndvdsadd  12569  gcdcllem1  12652  gcdcllem3  12654  1idssfct  12726  xpsff1o  13432  xpsmnd  14374  xpsgrp  14576  odlem1  14812  gexlem1  14852  dprdfeq0  15219  gsumdixp  15354  lspcl  15695  tgcl  16669  elcls  16772  opnnei  16819  cnpnei  16955  cmpcov2  17079  cmpfii  17098  txcnp  17276  xpstps  17463  fbun  17497  isfild  17515  snfil  17521  filcon  17540  isufil2  17565  hauspwpwf1  17644  xpsxms  18042  xpsms  18043  rlmnvc  18175  nmoid  18213  xrsmopn  18280  xrhmeo  18406  cphsqrcl  18582  iscmet3  18681  iundisj  18867  ioorinv  18893  plyexmo  19655  aalioulem3  19676  dvtaylp  19711  dvradcnv  19759  logtayllem  19968  logtayl  19969  musum  20393  pntlem3  20720  subgoablo  20938  ismndo2  20972  rngomndo  21048  sspval  21259  blo3i  21340  ajfval  21347  spanval  21872  cmcmlem  22130  cnvbraval  22650  leopnmid  22678  csmdsymi  22874  chirredlem4  22933  sumdmdlem  22958  ballotlemsdom  23031  ballotlemsel1i  23032  ballotlemsima  23035  ballotlemro  23042  ballotlemfrcn0  23049  ballotth  23057  cvmsdisj  23173  climuzcnv  23376  dfon2lem3  23510  dfon2lem7  23514  sspred  23543  sltval2  23678  axdenselem5  23708  imageval  23844  df3nandALT1  24210  lukshef-ax2  24229  arg-ax  24230  bibox  24348  binxt  24350  bidia  24355  evpexun  24364  difeqri2  24406  twsymr  24444  celsor  24477  dstr  24538  fisub  24921  cndpv  25416  gltpntl2  25440  xsyysx  25512  bsstrs  25513  nbssntrs  25514  pdiveql  25535  filnetlem2  25695  heiborlem3  25904  isfld2  25997  igenval2  26058  isfldidl  26060  dmncan2  26069  pellexlem5  26285  rmyabs  26412  jm2.24  26417  islssfgi  26537  pwslnm  26563  lindfind  26653  lindsind  26654  lindsind2  26656  lindff1  26657  f1linds  26662  islindf4  26675  dgraaub  26720  gsumcom3fi  26822  stoweidlem14  27098  stoweidlem15  27099  stoweidlem17  27101  stoweidlem35  27119  stoweidlem55  27139  stoweidlem57  27141  stoweidlem58  27142  stoweidlem59  27143  stoweid  27147  ee3bir  27317  vk15.4j  27344  onfrALTlem2  27364  a9e2nd  27377  dfvd1impr  27398  dfvd2impr  27426  e1bir  27452  e2bir  27455  e3bir  27564  19.21a3con13vVD  27678  3impexpbicomVD  27683  tratrbVD  27687  ssralv2VD  27692  truniALTVD  27704  trintALTVD  27706  undif3VD  27708  onfrALTlem3VD  27713  onfrALTlem2VD  27715  onfrALTVD  27717  relopabVD  27727  a9e2ndVD  27734  2uasbanhVD  27737  vk15.4jVD  27740  sspwimp  27744  sspwimpVD  27745  sspwimpcf  27746  sspwimpcfVD  27747  suctrALTcf  27748  suctrALTcfVD  27749  suctrALT3  27750  sspwimpALT  27751  unisnALT  27752  suctrALT4  27754  sspwimpALT2  27755  a9e2ndALT  27757  bnj1136  28076  bnj1175  28083  bnj1408  28115  albiiK  28159  ax6wfK  28181  ax6wK  28182  ax12OLD  28272  a12lem1  28297  lsat0cv  28390  pclfinclN  29306  docavalN  30480  djavalN  30492  dochval  30708  djhval  30755  dochexmidlem8  30824  dochkr1  30835  dochkr1OLDN  30836  hdmap1fval  31154
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator