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  1880  sbbii  1885  exmoeu  2155  eueq2  2876  ralun  3265  ssunieq  3758  ax9vsep  4042  ordunidif  4333  unizlim  4400  dfwe2  4464  onminex  4489  nnsuc  4564  opelxpi  4628  ndmima  4957  dffo2  5312  dff1o2  5334  resdif  5351  f1o00  5365  fvimacnvALT  5496  exfo  5530  ressnop0  5555  fsnunfv  5572  ovid  5816  ovidig  5817  f1stres  5993  f2ndres  5994  1st2val  5997  2nd2val  5998  frxp  6077  soxp  6080  tz7.49  6343  abianfp  6357  elixpsn  6741  domdifsn  6830  domunsncan  6847  fineqvlem  6962  unblem4  6997  ordiso2  7114  domwdom  7172  inf3lem3  7215  trcl  7294  unir1  7369  ssrankr1  7391  pm54.43lem  7516  infxpenlem  7525  ween  7546  acni3  7558  kmlem1  7660  infdif  7719  ackbij1lem1  7730  fin23lem14  7843  fin23lem32  7854  fin23lem40  7861  isfin1-3  7896  axcc2lem  7946  axdc3lem2  7961  axcclem  7967  ac6c4  7992  zornn0g  8016  axdclem2  8031  brdom3  8037  brdom5  8038  brdom4  8039  brdom6disj  8041  konigthlem  8070  pwcfsdom  8085  cfpwsdom  8086  alephom  8087  gruina  8320  grur1  8322  grothomex  8331  grothac  8332  nqpr  8518  axcnre  8666  axpre-sup  8671  ssxr  8772  le2tri3i  8829  0nn0  9859  uzind4  10155  rpnnen1lem5  10225  elfz4  10669  eluzfz  10671  hashxplem  11262  hashfun  11266  ccatswrd  11336  resqrex  11613  ndvdsadd  12481  gcdcllem1  12564  gcdcllem3  12566  1idssfct  12638  xpsff1o  13344  xpsmnd  14247  xpsgrp  14449  odlem1  14685  gexlem1  14725  dprdfeq0  15092  gsumdixp  15227  lspcl  15568  tgcl  16539  elcls  16642  opnnei  16689  cnpnei  16825  cmpcov2  16949  cmpfii  16968  txcnp  17146  xpstps  17333  fbun  17367  isfild  17385  snfil  17391  filcon  17410  isufil2  17435  hauspwpwf1  17514  xpsxms  17912  xpsms  17913  rlmnvc  18045  nmoid  18083  xrsmopn  18150  xrhmeo  18276  cphsqrcl  18452  iscmet3  18551  iundisj  18737  ioorinv  18763  plyexmo  19525  aalioulem3  19546  dvtaylp  19581  dvradcnv  19629  logtayllem  19838  logtayl  19839  musum  20263  pntlem3  20590  subgoablo  20808  ismndo2  20842  rngomndo  20918  sspval  21129  blo3i  21210  ajfval  21217  spanval  21742  cmcmlem  22018  cnvbraval  22520  leopnmid  22548  csmdsymi  22744  chirredlem4  22803  sumdmdlem  22828  cvmsdisj  22972  climuzcnv  23175  dfon2lem3  23309  dfon2lem7  23313  sspred  23342  sltval2  23477  axdenselem5  23507  imageval  23643  df3nandALT1  24009  lukshef-ax2  24028  arg-ax  24029  bibox  24147  binxt  24149  bidia  24154  evpexun  24163  difeqri2  24205  twsymr  24243  celsor  24276  dstr  24337  fisub  24720  cndpv  25215  gltpntl2  25239  xsyysx  25311  bsstrs  25312  nbssntrs  25313  pdiveql  25334  filnetlem2  25494  heiborlem3  25703  isfld2  25796  igenval2  25857  isfldidl  25859  dmncan2  25868  pellexlem5  26084  rmyabs  26211  jm2.24  26216  islssfgi  26336  pwslnm  26362  lindfind  26452  lindsind  26453  lindsind2  26455  lindff1  26456  f1linds  26461  islindf4  26474  dgraaub  26519  gsumcom3fi  26621  ee3bir  26957  vk15.4j  26984  onfrALTlem2  27004  a9e2nd  27017  dfvd1impr  27038  dfvd2impr  27066  e1bir  27092  e2bir  27095  e3bir  27204  19.21a3con13vVD  27318  3impexpbicomVD  27323  tratrbVD  27327  ssralv2VD  27332  truniALTVD  27344  trintALTVD  27346  undif3VD  27348  onfrALTlem3VD  27353  onfrALTlem2VD  27355  onfrALTVD  27357  relopabVD  27367  a9e2ndVD  27374  2uasbanhVD  27377  vk15.4jVD  27380  sspwimp  27384  sspwimpVD  27385  sspwimpcf  27386  sspwimpcfVD  27387  suctrALTcf  27388  suctrALTcfVD  27389  suctrALT3  27390  sspwimpALT  27391  unisnALT  27392  suctrALT4  27394  sspwimpALT2  27395  a9e2ndALT  27397  bnj1136  27716  bnj1175  27723  bnj1408  27755  ax12OLD  27794  a12lem1  27819  lsat0cv  27912  pclfinclN  28828  docavalN  30002  djavalN  30014  dochval  30230  djhval  30277  dochexmidlem8  30346  dochkr1  30357  dochkr1OLDN  30358  hdmap1fval  30676
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