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

Theorem biimpri 206
Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)
Hypothesis
Ref Expression
biimpri.1
Assertion
Ref Expression
biimpri

Proof of Theorem biimpri
StepHypRef Expression
1 biimpri.1 . . 3
21bicomi 202 . 2
32biimpi 194 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  mpbir  209  sylibr  212  sylbir  213  syl5bir  218  syl6ibr  227  bitri  249  mtbi  298  pm2.54  374  sylanbr  473  sylan2br  476  pm3.11  499  orbi2i  519  pm2.31  525  simplbi2  625  dfbi  629  pm2.85  853  rnlemOLD  965  syl3an1br  1267  syl3an2br  1268  syl3an3br  1269  nic-axALT  1507  speimfw  1735  sbbii  1746  exmidne  2662  eueq2  3273  ralun  3685  ssunieq  4284  ax6vsep  4577  ordunidif  4931  unizlim  4999  opelxpi  5036  ndmima  5378  funtpg  5643  dffo2  5804  dff1o2  5826  resdif  5841  f1o00  5853  fvimacnvALT  6006  fvcofneq  6039  exfo  6049  ressnop0  6078  fsnunfv  6111  ovid  6419  ovidig  6420  dfwe2  6617  onminex  6642  nnsuc  6717  1stnpr  6804  2ndnpr  6805  f1stres  6822  f2ndres  6823  1st2val  6826  2nd2val  6827  frxp  6910  soxp  6913  tz7.49  7129  elixpsn  7528  domdifsn  7620  domunsncan  7637  fineqvlem  7754  unblem4  7795  funsnfsupp  7873  ordiso2  7961  domwdom  8021  inf3lem3  8068  trcl  8180  unir1  8252  ssrankr1  8274  pm54.43lem  8401  infxpenlem  8412  ween  8437  acni3  8449  kmlem1  8551  infdif  8610  ackbij1lem1  8621  fin23lem14  8734  fin23lem32  8745  fin23lem40  8752  isfin1-3  8787  axcc2lem  8837  axdc3lem2  8852  axcclem  8858  ac6c4  8882  zornn0g  8906  axdclem2  8921  brdom3  8927  brdom5  8928  brdom4  8929  brdom6disj  8931  konigthlem  8964  pwcfsdom  8979  cfpwsdom  8980  alephom  8981  gruina  9217  grur1  9219  grothomex  9228  grothac  9229  nqpr  9413  axcnre  9562  axpre-sup  9567  ssxr  9675  le2tri3i  9735  0nn0  10835  uzind4  11168  rpnnen1lem5  11241  elfz4  11710  eluzfz  11712  ssfzo12bi  11907  hashgt0elex  12466  hashxplem  12491  hashfun  12495  ffz0iswrd  12568  wrdsymb1  12578  ccatfv0  12601  swrdn0  12655  ccatswrd  12681  repswfsts  12753  cshw1  12790  swrdco  12803  resqrex  13084  fsumsplitsnun  13570  ndvdsadd  14066  gcdcllem1  14149  gcdcllem3  14151  1idssfct  14223  cshwrepswhash1  14587  xpsff1o  14965  clatlem  15741  clatlubcl2  15743  clatglbcl2  15745  xpsmnd  15960  sgrp2rid2  16044  xpsgrp  16189  symg2bas  16423  symgextf  16442  gsmsymgrfix  16453  gsmsymgreqlem2  16456  pmtr3ncom  16500  odlem1  16559  gexlem1  16599  dprdfeq0  17062  dprdfeq0OLD  17069  gsumdixpOLD  17257  gsumdixp  17258  lspcl  17622  cply1mul  18335  psgndiflemB  18636  lindfind  18851  lindsind  18852  lindsind2  18854  lindff1  18855  f1linds  18860  gsumcom3fi  18902  mat1dimscm  18977  dmatmul  18999  mdetdiag  19101  mdetunilem7  19120  mdetunilem9  19122  madurid  19146  fvmptnn04if  19350  tgcl  19471  elcls  19574  opnnei  19621  neiptopnei  19633  cnpnei  19765  cmpcov2  19890  cmpfii  19909  txcnp  20121  xpstps  20311  fbun  20341  isfild  20359  snfil  20365  filcon  20384  isufil2  20409  hauspwpwf1  20488  cnextcn  20567  ustfilxp  20715  ustuqtop4  20747  xpsxms  21037  xpsms  21038  rlmnvc  21211  nmoid  21249  xrsmopn  21317  xrhmeo  21446  cphsqrtcl  21631  iscmet3  21732  rrxcph  21824  iundisj  21958  ioorinv  21985  plyexmo  22709  aalioulem3  22730  dvtaylp  22765  dvradcnv  22816  logtayllem  23040  logtayl  23041  musum  23467  pntlem3  23794  usgrarnedg  24384  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  nbcusgra  24463  wlkcpr  24529  2pthlem2  24598  nvnencycllem  24643  wlkiswwlk2lem1  24691  clwwlkel  24793  clwwlkf1  24796  clwlkf1clwwlklem  24849  2wlkonotv  24877  clwlknclwlkdifs  24960  frgra0v  24993  frgra3v  25002  2pthfrgrarn  25009  2pthfrgra  25011  n4cyclfrgra  25018  frgrancvvdeqlem9  25041  frgrawopreglem3  25046  frgraregorufr0  25052  numclwwlk2lem1  25102  subgoablo  25313  ismndo2  25347  rngomndo  25423  sspval  25636  blo3i  25717  ajfval  25724  spanval  26251  cmcmlem  26509  cnvbraval  27029  leopnmid  27057  csmdsymi  27253  chirredlem4  27312  sumdmdlem  27337  ceqsexv2d  27397  iundisjf  27448  rnct  27539  xrge0infss  27580  iundisjfi  27601  ishashinf  27606  xrpxdivcld  27631  pnfneige0  27933  rrhre  27999  logbid1  28014  esumcocn  28086  hasheuni  28091  sgon  28124  ddemeas  28208  1stmbfm  28231  2ndmbfm  28232  dya2iocct  28251  dya2iocnrect  28252  eulerpartgbij  28311  eulerpartlemgs2  28319  coinflippv  28422  cvmsdisj  28715  mrsubvrs  28882  mppspstlem  28931  problem4  29022  climuzcnv  29037  dfon2lem3  29217  dfon2lem7  29221  sspred  29252  sltval2  29416  nodenselem5  29445  imageval  29580  df3nandALT1  29862  lukshef-ax2  29880  arg-ax  29881  finixpnum  30038  fin2solem  30039  mblfinlem3  30053  itg2addnclem2  30067  itg2addnc  30069  bddiblnc  30085  ftc1anclem6  30095  filnetlem2  30197  heiborlem3  30309  isfld2  30402  igenval2  30463  isfldidl  30465  dmncan2  30474  oprabbi  30570  mpt2bi123f  30571  opabbi  30574  ac6s3f  30579  pellexlem5  30769  rmyabs  30896  jm2.24  30901  islssfgi  31018  pwslnm  31040  dgraaub  31097  infrglb  31584  cncfuni  31689  iblcncfioo  31777  stoweidlem14  31796  stoweidlem17  31799  stoweidlem35  31817  stoweidlem57  31839  stirlinglem7  31862  stirlinglem10  31865  fourierdlem54  31943  fourierdlem62  31951  fourierdlem63  31952  fourierdlem65  31954  fourierdlem73  31962  fourierdlem80  31969  fourierdlem82  31971  fourierdlem101  31990  etransclem32  32049  aibandbiaiaiffb  32090  fnresfnco  32211  dfdfat2  32216  afvres  32257  tz6.12-afv  32258  ndmaovass  32291  2f1fvneq  32307  el2fzo  32339  fzoopth  32340  lswn0  32343  spthdifv  32352  euelss  32553  initoeu2  32622  lincext1  33055  3impexpbicom  33221  ee3bir  33272  vk15.4j  33298  onfrALTlem2  33318  ax6e2nd  33331  dfvd1impr  33353  dfvd2impr  33390  e1bir  33416  e2bir  33419  e3bir  33536  suctrALT  33626  19.21a3con13vVD  33652  3impexpbicomVD  33657  tratrbVD  33661  ssralv2VD  33666  truniALTVD  33678  trintALTVD  33680  undif3VD  33682  onfrALTlem3VD  33687  onfrALTlem2VD  33689  onfrALTVD  33691  relopabVD  33701  ax6e2ndVD  33708  2uasbanhVD  33711  vk15.4jVD  33714  sspwimp  33718  sspwimpVD  33719  sspwimpcf  33720  sspwimpcfVD  33721  suctrALTcf  33722  suctrALTcfVD  33723  suctrALT3  33724  sspwimpALT  33725  unisnALT  33726  ax6e2ndALT  33730  isosctrlem1ALT  33734  iunconlem2  33735  bnj1136  34053  bnj1175  34060  bnj1408  34092  sylbbr  34133  sylbb1  34134  sylbb2  34135  sylancl3  34169  bj-andnotim  34177  bj-modalbe  34241  bj-2uplex  34580  lsat0cv  34758  pclfinclN  35674  docavalN  36850  djavalN  36862  dochval  37078  djhval  37125  dochexmidlem8  37194  dochkr1  37205  dochkr1OLDN  37206  hdmap1fval  37524  xptrrel  37775  cotr2g  37786  frege55lem1a  37893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator