MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpri Structured version   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 4    <-> 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  610  dfbi  612  pm2.85  828  rnlem  933  syl3an1br  1224  syl3an2br  1225  syl3an3br  1226  3impexpbicom  1377  nic-axALT  1449  sbbii  1666  hbn1fw  1720  hbn1fwOLD  1721  equveliOLD  2087  exmoeu  2325  eueq2  3110  ralun  3531  ssunieq  4050  ax9vsep  4336  ordunidif  4631  suctr  4667  unizlim  4700  dfwe2  4764  onminex  4789  nnsuc  4864  opelxpi  4912  ndmima  5243  funtpg  5503  dffo2  5659  dff1o2  5681  resdif  5698  f1o00  5712  fvimacnvALT  5851  exfo  5889  ressnop0  5915  fsnunfv  5935  ovid  6192  ovidig  6193  f1stres  6370  f2ndres  6371  1st2val  6374  2nd2val  6375  frxp  6458  soxp  6461  tz7.49  6704  abianfp  6718  elixpsn  7103  domdifsn  7193  domunsncan  7210  fineqvlem  7325  unblem4  7364  ordiso2  7486  domwdom  7544  inf3lem3  7587  trcl  7666  unir1  7741  ssrankr1  7763  pm54.43lem  7888  infxpenlem  7897  ween  7918  acni3  7930  kmlem1  8032  infdif  8091  ackbij1lem1  8102  fin23lem14  8215  fin23lem32  8226  fin23lem40  8233  isfin1-3  8268  axcc2lem  8318  axdc3lem2  8333  axcclem  8339  ac6c4  8363  zornn0g  8387  axdclem2  8402  brdom3  8408  brdom5  8409  brdom4  8410  brdom6disj  8412  konigthlem  8445  pwcfsdom  8460  cfpwsdom  8461  alephom  8462  gruina  8695  grur1  8697  grothomex  8706  grothac  8707  nqpr  8893  axcnre  9041  axpre-sup  9046  ssxr  9147  le2tri3i  9205  0nn0  10238  uzind4  10536  rpnnen1lem5  10606  elfz4  11054  eluzfz  11056  hashgt0elex  11672  hashxplem  11698  hashfun  11702  ccatswrd  11775  resqrex  12058  ndvdsadd  12930  gcdcllem1  13013  gcdcllem3  13015  1idssfct  13087  xpsff1o  13795  xpsmnd  14737  xpsgrp  14939  odlem1  15175  gexlem1  15215  dprdfeq0  15582  gsumdixp  15717  lspcl  16054  tgcl  17036  elcls  17139  opnnei  17186  neiptopnei  17198  cnpnei  17330  cmpcov2  17455  cmpfii  17474  txcnp  17654  xpstps  17844  fbun  17874  isfild  17892  snfil  17898  filcon  17917  isufil2  17942  hauspwpwf1  18021  cnextcn  18100  ustfilxp  18244  ustuqtop4  18276  xpsxms  18566  xpsms  18567  rlmnvc  18740  nmoid  18778  xrsmopn  18845  xrhmeo  18973  cphsqrcl  19149  iscmet3  19248  iundisj  19444  ioorinv  19470  plyexmo  20232  aalioulem3  20253  dvtaylp  20288  dvradcnv  20339  logtayllem  20552  logtayl  20553  musum  20978  pntlem3  21305  usgrarnedg  21406  nb3grapr  21464  nb3grapr2  21465  nb3gra2nb  21466  nbcusgra  21474  2pthlem2  21598  nvnencycllem  21632  subgoablo  21901  ismndo2  21935  rngomndo  22011  sspval  22224  blo3i  22305  ajfval  22312  spanval  22837  cmcmlem  23095  cnvbraval  23615  leopnmid  23643  csmdsymi  23839  chirredlem4  23898  sumdmdlem  23923  ceqsexv2d  23987  iundisjf  24031  1stnpr  24095  2ndnpr  24096  rnct  24110  iundisjfi  24154  ishashinf  24161  xrpxdivcld  24183  pnfneige0  24338  rrhre  24389  logbid1  24400  esumcocn  24472  hasheuni  24477  sgon  24509  1stmbfm  24612  2ndmbfm  24613  dya2iocct  24632  dya2iocnrect  24633  sibfof  24656  coinflippv  24743  cvmsdisj  24959  climuzcnv  25110  dfon2lem3  25414  dfon2lem7  25418  sspred  25449  sltval2  25613  nodenselem5  25642  imageval  25777  df3nandALT1  26148  lukshef-ax2  26167  arg-ax  26168  mblfinlem3  26247  itg2addnclem2  26259  itg2addnc  26261  bddiblnc  26277  ftc1anclem6  26287  filnetlem2  26410  heiborlem3  26524  isfld2  26617  igenval2  26678  isfldidl  26680  dmncan2  26689  pellexlem5  26898  rmyabs  27025  jm2.24  27030  islssfgi  27149  pwslnm  27175  lindfind  27265  lindsind  27266  lindsind2  27268  lindff1  27269  f1linds  27274  islindf4  27287  dgraaub  27332  gsumcom3fi  27434  infrglb  27700  stoweidlem14  27741  stoweidlem17  27744  stoweidlem35  27762  stoweidlem55  27782  stoweidlem57  27784  stoweid  27790  stirlinglem7  27807  stirlinglem10  27810  aibandbiaiaiffb  27841  fnresfnco  27968  dfdfat2  27973  afvres  28014  tz6.12-afv  28015  ndmaovass  28048  2f1fvneq  28083  el2fzo  28149  fzoopth  28150  wrdsymb1  28194  ccatsymb  28199  lswrdn0  28282  cshw1  28297  cshw1v  28298  cshwssizelem2  28303  spthdifv  28335  wlkiswwlk2lem1  28361  2wlkonotv  28397  frgra0v  28445  frgra3v  28454  2pthfrgrarn  28461  2pthfrgra  28463  n4cyclfrgra  28470  frgrancvvdeqlem9  28492  frgrawopreglem3  28497  frgraregorufr0  28503  ee3bir  28647  vk15.4j  28674  onfrALTlem2  28694  a9e2nd  28707  dfvd1impr  28730  dfvd2impr  28767  e1bir  28793  e2bir  28796  e3bir  28913  19.21a3con13vVD  29026  3impexpbicomVD  29031  tratrbVD  29035  ssralv2VD  29040  truniALTVD  29052  trintALTVD  29054  undif3VD  29056  onfrALTlem3VD  29061  onfrALTlem2VD  29063  onfrALTVD  29065  relopabVD  29075  a9e2ndVD  29082  2uasbanhVD  29085  vk15.4jVD  29088  sspwimp  29092  sspwimpVD  29093  sspwimpcf  29094  sspwimpcfVD  29095  suctrALTcf  29096  suctrALTcfVD  29097  suctrALT3  29098  sspwimpALT  29099  unisnALT  29100  a9e2ndALT  29104  isosctrlem1ALT  29108  iunconlem2  29109  bnj1136  29428  bnj1175  29435  bnj1408  29467  equveliNEW7  29590  ax7w10AUX7  29724  lsat0cv  29893  pclfinclN  30809  docavalN  31983  djavalN  31995  dochval  32211  djhval  32258  dochexmidlem8  32327  dochkr1  32338  dochkr1OLDN  32339  hdmap1fval  32657
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 179
  Copyright terms: Public domain W3C validator