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  1643  hbn1fw  1691  equveli  1941  exmoeu  2198  eueq2  2952  ralun  3370  ssunieq  3876  ax9vsep  4161  ordunidif  4456  unizlim  4525  dfwe2  4589  onminex  4614  nnsuc  4689  opelxpi  4737  ndmima  5066  dffo2  5471  dff1o2  5493  resdif  5510  f1o00  5524  fvimacnvALT  5660  exfo  5694  ressnop0  5719  fsnunfv  5736  ovid  5980  ovidig  5981  f1stres  6157  f2ndres  6158  1st2val  6161  2nd2val  6162  frxp  6241  soxp  6244  tz7.49  6473  abianfp  6487  elixpsn  6871  domdifsn  6961  domunsncan  6978  fineqvlem  7093  unblem4  7128  ordiso2  7246  domwdom  7304  inf3lem3  7347  trcl  7426  unir1  7501  ssrankr1  7523  pm54.43lem  7648  infxpenlem  7657  ween  7678  acni3  7690  kmlem1  7792  infdif  7851  ackbij1lem1  7862  fin23lem14  7975  fin23lem32  7986  fin23lem40  7993  isfin1-3  8028  axcc2lem  8078  axdc3lem2  8093  axcclem  8099  ac6c4  8124  zornn0g  8148  axdclem2  8163  brdom3  8169  brdom5  8170  brdom4  8171  brdom6disj  8173  konigthlem  8206  pwcfsdom  8221  cfpwsdom  8222  alephom  8223  gruina  8456  grur1  8458  grothomex  8467  grothac  8468  nqpr  8654  axcnre  8802  axpre-sup  8807  ssxr  8908  le2tri3i  8965  0nn0  9996  uzind4  10292  rpnnen1lem5  10362  elfz4  10807  eluzfz  10809  hashxplem  11401  hashfun  11405  ccatswrd  11475  resqrex  11752  ndvdsadd  12623  gcdcllem1  12706  gcdcllem3  12708  1idssfct  12780  xpsff1o  13486  xpsmnd  14428  xpsgrp  14630  odlem1  14866  gexlem1  14906  dprdfeq0  15273  gsumdixp  15408  lspcl  15749  tgcl  16723  elcls  16826  opnnei  16873  cnpnei  17009  cmpcov2  17133  cmpfii  17152  txcnp  17330  xpstps  17517  fbun  17551  isfild  17569  snfil  17575  filcon  17594  isufil2  17619  hauspwpwf1  17698  xpsxms  18096  xpsms  18097  rlmnvc  18229  nmoid  18267  xrsmopn  18334  xrhmeo  18460  cphsqrcl  18636  iscmet3  18735  iundisj  18921  ioorinv  18947  plyexmo  19709  aalioulem3  19730  dvtaylp  19765  dvradcnv  19813  logtayllem  20022  logtayl  20023  musum  20447  pntlem3  20774  subgoablo  20994  ismndo2  21028  rngomndo  21104  sspval  21315  blo3i  21396  ajfval  21403  spanval  21928  cmcmlem  22186  cnvbraval  22706  leopnmid  22734  csmdsymi  22930  chirredlem4  22989  sumdmdlem  23014  ballotlemsdom  23086  ballotlemsel1i  23087  ballotlemsima  23090  ballotlemro  23097  ballotlemfrcn0  23104  ballotth  23112  xrpxdivcld  23135  ceqsexv2d  23178  rnmpt2ss  23254  1stnpr  23260  2ndnpr  23261  ssnnssfz  23292  xrge0iifmhm  23336  fsumrp0cl  23349  rnct  23359  iundisjfi  23378  iundisjf  23380  pnfneige0  23389  ishashinf  23404  logbid1  23415  esumle  23448  esumlef  23450  esumcst  23451  esumpinfval  23456  esumpcvgval  23461  esumcocn  23463  hasheuni  23468  esumcvg  23469  sgon  23500  sigagenss  23525  sigagenid  23526  1stmbfm  23580  2ndmbfm  23581  imambfm  23582  dya2iocct  23596  probmeasb  23648  coinflippv  23699  cvmsdisj  23816  climuzcnv  24019  dfon2lem3  24212  dfon2lem7  24216  sspred  24245  sltval2  24381  nodenselem5  24410  imageval  24540  df3nandALT1  24907  lukshef-ax2  24926  arg-ax  24927  itg2addnclem2  25004  bddiblnc  25021  bibox  25085  binxt  25087  bidia  25092  evpexun  25101  difeqri2  25143  twsymr  25181  celsor  25214  dstr  25274  fisub  25657  cndpv  26152  gltpntl2  26176  xsyysx  26248  bsstrs  26249  nbssntrs  26250  pdiveql  26271  filnetlem2  26431  heiborlem3  26640  isfld2  26733  igenval2  26794  isfldidl  26796  dmncan2  26805  pellexlem5  27021  rmyabs  27148  jm2.24  27153  islssfgi  27273  pwslnm  27299  lindfind  27389  lindsind  27390  lindsind2  27392  lindff1  27393  f1linds  27398  islindf4  27411  dgraaub  27456  gsumcom3fi  27558  infrglb  27825  stoweidlem14  27866  stoweidlem15  27867  stoweidlem17  27869  stoweidlem35  27887  stoweidlem55  27907  stoweidlem57  27909  stoweidlem58  27910  stoweidlem59  27911  stoweid  27915  stirlinglem7  27932  stirlinglem10  27935  stirlinglem12  27937  fnresfnco  28094  dfdfat2  28099  afvres  28140  tz6.12-afv  28141  ndmaovass  28174  nb3grapr  28289  nb3grapr2  28290  nb3gra2nb  28291  nbcusgra  28298  nvnencycllem  28389  frgra0v  28420  2pthfrgrarn  28433  n4cyclfrgra  28440  ee3bir  28563  vk15.4j  28590  onfrALTlem2  28610  a9e2nd  28623  dfvd1impr  28644  dfvd2impr  28681  e1bir  28707  e2bir  28710  e3bir  28828  19.21a3con13vVD  28944  3impexpbicomVD  28949  tratrbVD  28953  ssralv2VD  28958  truniALTVD  28970  trintALTVD  28972  undif3VD  28974  onfrALTlem3VD  28979  onfrALTlem2VD  28981  onfrALTVD  28983  relopabVD  28993  a9e2ndVD  29000  2uasbanhVD  29003  vk15.4jVD  29006  sspwimp  29010  sspwimpVD  29011  sspwimpcf  29012  sspwimpcfVD  29013  suctrALTcf  29014  suctrALTcfVD  29015  suctrALT3  29016  sspwimpALT  29017  unisnALT  29018  suctrALT4  29020  sspwimpALT2  29021  a9e2ndALT  29023  bnj1136  29343  bnj1175  29350  bnj1408  29382  equveliNEW7  29503  ax12OLD  29727  a12lem1  29752  lsat0cv  29845  pclfinclN  30761  docavalN  31935  djavalN  31947  dochval  32163  djhval  32210  dochexmidlem8  32279  dochkr1  32290  dochkr1OLDN  32291  hdmap1fval  32609
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