MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpri 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  1373  nic-axALT  1445  sbbii  1660  hbn1fw  1712  equveli  2025  exmoeu  2281  eueq2  3052  ralun  3473  ssunieq  3991  ax9vsep  4276  ordunidif  4571  unizlim  4639  dfwe2  4703  onminex  4728  nnsuc  4803  opelxpi  4851  ndmima  5182  funtpg  5442  dffo2  5598  dff1o2  5620  resdif  5637  f1o00  5651  fvimacnvALT  5789  exfo  5827  ressnop0  5853  fsnunfv  5873  ovid  6130  ovidig  6131  f1stres  6308  f2ndres  6309  1st2val  6312  2nd2val  6313  frxp  6393  soxp  6396  tz7.49  6639  abianfp  6653  elixpsn  7038  domdifsn  7128  domunsncan  7145  fineqvlem  7260  unblem4  7299  ordiso2  7418  domwdom  7476  inf3lem3  7519  trcl  7598  unir1  7673  ssrankr1  7695  pm54.43lem  7820  infxpenlem  7829  ween  7850  acni3  7862  kmlem1  7964  infdif  8023  ackbij1lem1  8034  fin23lem14  8147  fin23lem32  8158  fin23lem40  8165  isfin1-3  8200  axcc2lem  8250  axdc3lem2  8265  axcclem  8271  ac6c4  8295  zornn0g  8319  axdclem2  8334  brdom3  8340  brdom5  8341  brdom4  8342  brdom6disj  8344  konigthlem  8377  pwcfsdom  8392  cfpwsdom  8393  alephom  8394  gruina  8627  grur1  8629  grothomex  8638  grothac  8639  nqpr  8825  axcnre  8973  axpre-sup  8978  ssxr  9079  le2tri3i  9136  0nn0  10169  uzind4  10467  rpnnen1lem5  10537  elfz4  10985  eluzfz  10987  hashgt0elex  11598  hashxplem  11624  hashfun  11628  ccatswrd  11701  resqrex  11984  ndvdsadd  12856  gcdcllem1  12939  gcdcllem3  12941  1idssfct  13013  xpsff1o  13721  xpsmnd  14663  xpsgrp  14865  odlem1  15101  gexlem1  15141  dprdfeq0  15508  gsumdixp  15643  lspcl  15980  tgcl  16958  elcls  17061  opnnei  17108  neiptopnei  17120  cnpnei  17251  cmpcov2  17376  cmpfii  17395  txcnp  17574  xpstps  17764  fbun  17794  isfild  17812  snfil  17818  filcon  17837  isufil2  17862  hauspwpwf1  17941  cnextcn  18020  ustfilxp  18164  ustuqtop4  18196  xpsxms  18455  xpsms  18456  rlmnvc  18610  nmoid  18648  xrsmopn  18715  xrhmeo  18843  cphsqrcl  19019  iscmet3  19118  iundisj  19310  ioorinv  19336  plyexmo  20098  aalioulem3  20119  dvtaylp  20154  dvradcnv  20205  logtayllem  20418  logtayl  20419  musum  20844  pntlem3  21171  usgrarnedg  21271  nb3grapr  21329  nb3grapr2  21330  nb3gra2nb  21331  nbcusgra  21339  2pthonlem2  21449  nvnencycllem  21479  subgoablo  21748  ismndo2  21782  rngomndo  21858  sspval  22071  blo3i  22152  ajfval  22159  spanval  22684  cmcmlem  22942  cnvbraval  23462  leopnmid  23490  csmdsymi  23686  chirredlem4  23745  sumdmdlem  23770  ceqsexv2d  23830  iundisjf  23873  1stnpr  23935  2ndnpr  23936  rnct  23950  iundisjfi  23991  ishashinf  23998  xrpxdivcld  24021  pnfneige0  24141  rrhre  24184  logbid1  24195  esumcocn  24267  hasheuni  24272  sgon  24304  1stmbfm  24405  2ndmbfm  24406  dya2iocct  24425  dya2iocnrect  24426  coinflippv  24521  cvmsdisj  24737  climuzcnv  24888  dfon2lem3  25166  dfon2lem7  25170  sspred  25199  sltval2  25335  nodenselem5  25364  imageval  25494  df3nandALT1  25861  lukshef-ax2  25880  arg-ax  25881  itg2addnclem2  25959  bddiblnc  25976  filnetlem2  26100  heiborlem3  26214  isfld2  26307  igenval2  26368  isfldidl  26370  dmncan2  26379  pellexlem5  26588  rmyabs  26715  jm2.24  26720  islssfgi  26840  pwslnm  26866  lindfind  26956  lindsind  26957  lindsind2  26959  lindff1  26960  f1linds  26965  islindf4  26978  dgraaub  27023  gsumcom3fi  27125  infrglb  27391  stoweidlem14  27432  stoweidlem17  27435  stoweidlem35  27453  stoweidlem55  27473  stoweidlem57  27475  stoweid  27481  stirlinglem7  27498  stirlinglem10  27501  aibandbiaiaiffb  27532  fnresfnco  27660  dfdfat2  27665  afvres  27706  tz6.12-afv  27707  ndmaovass  27740  frgra0v  27747  frgra3v  27756  2pthfrgrarn  27763  2pthfrgra  27765  n4cyclfrgra  27772  frgrancvvdeqlem9  27794  frgrawopreglem3  27799  frgraregorufr0  27805  ee3bir  27929  vk15.4j  27956  onfrALTlem2  27976  a9e2nd  27989  dfvd1impr  28010  dfvd2impr  28047  e1bir  28073  e2bir  28076  e3bir  28193  19.21a3con13vVD  28306  3impexpbicomVD  28311  tratrbVD  28315  ssralv2VD  28320  truniALTVD  28332  trintALTVD  28334  undif3VD  28336  onfrALTlem3VD  28341  onfrALTlem2VD  28343  onfrALTVD  28345  relopabVD  28355  a9e2ndVD  28362  2uasbanhVD  28365  vk15.4jVD  28368  sspwimp  28372  sspwimpVD  28373  sspwimpcf  28374  sspwimpcfVD  28375  suctrALTcf  28376  suctrALTcfVD  28377  suctrALT3  28378  sspwimpALT  28379  unisnALT  28380  a9e2ndALT  28385  bnj1136  28705  bnj1175  28712  bnj1408  28744  equveliNEW7  28865  lsat0cv  29149  pclfinclN  30065  docavalN  31239  djavalN  31251  dochval  31467  djhval  31514  dochexmidlem8  31583  dochkr1  31594  dochkr1OLDN  31595  hdmap1fval  31913
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