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

Theorem biimpri 197
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 193 . 2  |-  ( ps  <->  ph )
32biimpi 186 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  mpbir  200  sylibr  203  sylbir  204  syl5bir  209  syl6ibr  218  bitri  240  mtbi  289  pm2.54  363  sylanbr  459  sylan2br  462  pm3.11  485  orbi2i  505  pm2.31  511  simplbi2  608  dfbi  610  pm2.85  826  rnlem  931  syl3an1br  1221  syl3an2br  1222  syl3an3br  1223  3impexpbicom  1357  nic-axALT  1429  sbbii  1634  hbn1fw  1679  equveli  1928  exmoeu  2185  eueq2  2939  ralun  3357  ssunieq  3860  ax9vsep  4145  ordunidif  4440  unizlim  4509  dfwe2  4573  onminex  4598  nnsuc  4673  opelxpi  4721  ndmima  5050  dffo2  5455  dff1o2  5477  resdif  5494  f1o00  5508  fvimacnvALT  5644  exfo  5678  ressnop0  5703  fsnunfv  5720  ovid  5964  ovidig  5965  f1stres  6141  f2ndres  6142  1st2val  6145  2nd2val  6146  frxp  6225  soxp  6228  tz7.49  6457  abianfp  6471  elixpsn  6855  domdifsn  6945  domunsncan  6962  fineqvlem  7077  unblem4  7112  ordiso2  7230  domwdom  7288  inf3lem3  7331  trcl  7410  unir1  7485  ssrankr1  7507  pm54.43lem  7632  infxpenlem  7641  ween  7662  acni3  7674  kmlem1  7776  infdif  7835  ackbij1lem1  7846  fin23lem14  7959  fin23lem32  7970  fin23lem40  7977  isfin1-3  8012  axcc2lem  8062  axdc3lem2  8077  axcclem  8083  ac6c4  8108  zornn0g  8132  axdclem2  8147  brdom3  8153  brdom5  8154  brdom4  8155  brdom6disj  8157  konigthlem  8190  pwcfsdom  8205  cfpwsdom  8206  alephom  8207  gruina  8440  grur1  8442  grothomex  8451  grothac  8452  nqpr  8638  axcnre  8786  axpre-sup  8791  ssxr  8892  le2tri3i  8949  0nn0  9980  uzind4  10276  rpnnen1lem5  10346  elfz4  10791  eluzfz  10793  hashxplem  11385  hashfun  11389  ccatswrd  11459  resqrex  11736  ndvdsadd  12607  gcdcllem1  12690  gcdcllem3  12692  1idssfct  12764  xpsff1o  13470  xpsmnd  14412  xpsgrp  14614  odlem1  14850  gexlem1  14890  dprdfeq0  15257  gsumdixp  15392  lspcl  15733  tgcl  16707  elcls  16810  opnnei  16857  cnpnei  16993  cmpcov2  17117  cmpfii  17136  txcnp  17314  xpstps  17501  fbun  17535  isfild  17553  snfil  17559  filcon  17578  isufil2  17603  hauspwpwf1  17682  xpsxms  18080  xpsms  18081  rlmnvc  18213  nmoid  18251  xrsmopn  18318  xrhmeo  18444  cphsqrcl  18620  iscmet3  18719  iundisj  18905  ioorinv  18931  plyexmo  19693  aalioulem3  19714  dvtaylp  19749  dvradcnv  19797  logtayllem  20006  logtayl  20007  musum  20431  pntlem3  20758  subgoablo  20978  ismndo2  21012  rngomndo  21088  sspval  21299  blo3i  21380  ajfval  21387  spanval  21912  cmcmlem  22170  cnvbraval  22690  leopnmid  22718  csmdsymi  22914  chirredlem4  22973  sumdmdlem  22998  ballotlemsdom  23070  ballotlemsel1i  23071  ballotlemsima  23074  ballotlemro  23081  ballotlemfrcn0  23088  ballotth  23096  xrpxdivcld  23119  ceqsexv2d  23162  rnmpt2ss  23239  1stnpr  23245  2ndnpr  23246  ssnnssfz  23277  xrge0iifmhm  23321  fsumrp0cl  23334  rnct  23344  iundisjfi  23363  iundisjf  23365  pnfneige0  23374  ishashinf  23389  logbid1  23400  esumle  23433  esumlef  23435  esumcst  23436  esumpinfval  23441  esumpcvgval  23446  esumcocn  23448  hasheuni  23453  esumcvg  23454  sgon  23485  sigagenss  23510  sigagenid  23511  1stmbfm  23565  2ndmbfm  23566  imambfm  23567  dya2iocct  23581  probmeasb  23633  coinflippv  23684  cvmsdisj  23801  climuzcnv  24004  dfon2lem3  24141  dfon2lem7  24145  sspred  24174  sltval2  24310  nodenselem5  24339  imageval  24469  df3nandALT1  24835  lukshef-ax2  24854  arg-ax  24855  bibox  24982  binxt  24984  bidia  24989  evpexun  24998  difeqri2  25040  twsymr  25078  celsor  25111  dstr  25171  fisub  25554  cndpv  26049  gltpntl2  26073  xsyysx  26145  bsstrs  26146  nbssntrs  26147  pdiveql  26168  filnetlem2  26328  heiborlem3  26537  isfld2  26630  igenval2  26691  isfldidl  26693  dmncan2  26702  pellexlem5  26918  rmyabs  27045  jm2.24  27050  islssfgi  27170  pwslnm  27196  lindfind  27286  lindsind  27287  lindsind2  27289  lindff1  27290  f1linds  27295  islindf4  27308  dgraaub  27353  gsumcom3fi  27455  infrglb  27722  stoweidlem14  27763  stoweidlem15  27764  stoweidlem17  27766  stoweidlem35  27784  stoweidlem55  27804  stoweidlem57  27806  stoweidlem58  27807  stoweidlem59  27808  stoweid  27812  stirlinglem7  27829  stirlinglem10  27832  stirlinglem12  27834  fnresfnco  27989  dfdfat2  27994  afvres  28034  ndmaovass  28066  nbcusgra  28159  frgra0v  28174  ee3bir  28264  vk15.4j  28291  onfrALTlem2  28311  a9e2nd  28324  dfvd1impr  28345  dfvd2impr  28376  e1bir  28402  e2bir  28405  e3bir  28514  19.21a3con13vVD  28628  3impexpbicomVD  28633  tratrbVD  28637  ssralv2VD  28642  truniALTVD  28654  trintALTVD  28656  undif3VD  28658  onfrALTlem3VD  28663  onfrALTlem2VD  28665  onfrALTVD  28667  relopabVD  28677  a9e2ndVD  28684  2uasbanhVD  28687  vk15.4jVD  28690  sspwimp  28694  sspwimpVD  28695  sspwimpcf  28696  sspwimpcfVD  28697  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT3  28700  sspwimpALT  28701  unisnALT  28702  suctrALT4  28704  sspwimpALT2  28705  a9e2ndALT  28707  bnj1136  29027  bnj1175  29034  bnj1408  29066  ax12OLD  29105  a12lem1  29130  lsat0cv  29223  pclfinclN  30139  docavalN  31313  djavalN  31325  dochval  31541  djhval  31588  dochexmidlem8  31657  dochkr1  31668  dochkr1OLDN  31669  hdmap1fval  31987
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 177
  Copyright terms: Public domain W3C validator