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

Theorem biimpri 218
Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 210. (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 214 . 2 (𝜓𝜑)
32biimpi 206 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  mpbir  221  sylibr  224  sylbir  225  sylbbr  226  sylbb1  227  sylbb2  228  syl5bir  233  syl6ibr  242  mtbi  312  pm2.54  389  sylanbr  490  sylan2br  493  pm3.11  520  orbi2i  541  pm2.31  547  simplbi2  654  dfbi  660  sylanblrc  696  pm2.85  897  pm3.2an3  1238  syl3an1br  1363  syl3an2br  1364  syl3an3br  1365  had1  1540  nic-axALT  1597  speimfw  1874  sbbii  1885  ceqsexv2d  3238  eueq2  3374  ralun  3787  ssunieq  4463  ax6vsep  4776  opelxpi  5138  elsnxpOLD  5666  ordunidif  5761  unizlim  5832  funtpgOLD  5931  dffo2  6106  dff1o2  6129  resdif  6144  f1o00  6158  fvimacnvALT  6322  fvcofneq  6353  exfo  6363  ressnop0  6405  fsnunfv  6438  2f1fvneq  6502  ovid  6762  ovidig  6763  dfwe2  6966  onminex  6992  nnsuc  7067  1stnpr  7157  2ndnpr  7158  f1stres  7175  f2ndres  7176  1st2val  7179  2nd2val  7180  frxp  7272  soxp  7275  tz7.49  7525  elixpsn  7932  domdifsn  8028  domunsncan  8045  fineqvlem  8159  unblem4  8200  ordiso2  8405  domwdom  8464  zfreg  8485  inf3lem3  8512  trcl  8589  unir1  8661  ssrankr1  8683  pm54.43lem  8810  infxpenlem  8821  ween  8843  acni3  8855  kmlem1  8957  infdif  9016  ackbij1lem1  9027  fin23lem14  9140  fin23lem32  9151  isfin1-3  9193  axcc2lem  9243  axdc3lem2  9258  ac6c4  9288  zornn0g  9312  axdclem2  9327  rnct  9332  brdom3  9335  brdom5  9336  brdom4  9337  brdom6disj  9339  konigthlem  9375  pwcfsdom  9390  cfpwsdom  9391  alephom  9392  gruina  9625  grur1  9627  grothomex  9636  grothac  9637  nqpr  9821  axcnre  9970  axpre-sup  9975  ssxr  10092  le2tri3i  10152  muldivdir  10705  0nn0  11292  uzind4  11731  rpnnen1lem5  11803  rpnnen1lem5OLD  11809  elfz4  12320  eluzfz  12322  ssfzo12bi  12547  hashgt0elex  13172  hashxplem  13203  hashfun  13207  ishashinf  13230  ffz0iswrd  13315  wrdsymb1  13325  ccatfv0  13350  lswccats1fst  13394  ccatswrd  13438  repswfsts  13509  cshinj  13538  cshw1  13549  swrdco  13564  cotr2g  13696  xptrrel  13700  trclun  13736  resqrex  13972  pwm1geoser  14581  sumeven  15091  ndvdsadd  15115  gcdcllem1  15202  gcdcllem3  15204  lcmftp  15330  lcmfunsnlem2lem2  15333  lcmfunsnlem2  15334  lcmfun  15339  ncoprmgcdne1b  15344  coprmprod  15356  coprmproddvdslem  15357  divgcdcoprmex  15361  1idssfct  15374  prmodvdslcmf  15732  cshwrepswhash1  15790  xpsff1o  16209  initoeu2  16647  clatlem  17092  clatlubcl2  17094  clatglbcl2  17096  xpsmnd  17311  sgrp2rid2  17394  xpsgrp  17515  symg2bas  17799  symgextf  17818  gsmsymgrfix  17829  gsmsymgreqlem2  17832  pmtr3ncom  17876  odlem1  17935  gexlem1  17975  dprdfeq0  18402  gsumdixp  18590  lspcl  18957  cply1mul  19645  psgndiflemB  19927  lindfind  20136  lindsind  20137  lindsind2  20139  lindff1  20140  f1linds  20145  gsumcom3fi  20187  mat1dimscm  20262  dmatmul  20284  mdetdiag  20386  mdetunilem7  20405  mdetunilem9  20407  madurid  20431  fvmptnn04if  20635  toprntopon  20710  tgcl  20754  elcls  20858  opnnei  20905  neiptopnei  20917  cnpnei  21049  cmpfii  21193  txcnp  21404  xpstps  21594  fbun  21625  isfild  21643  snfil  21649  filconn  21668  isufil2  21693  hauspwpwf1  21772  cnextcn  21852  ustfilxp  21997  ustuqtop4  22029  xpsxms  22320  xpsms  22321  rlmnvc  22488  nmoid  22527  xrsmopn  22596  xrhmeo  22726  cphsqrtcl  22965  iscmet3  23072  iundisj  23297  ioorinv  23325  plyexmo  24049  aalioulem3  24070  dvtaylp  24105  dvradcnv  24156  logtayllem  24386  logtayl  24387  logbid1  24487  logbchbase  24490  relogbcxpb  24506  logbmpt  24507  logbfval  24509  musum  24898  lgsmodeq  25048  lgsmulsqcoprm  25049  2lgs  25113  pntlem3  25279  nbupgrel  26222  nbusgrvtxm1  26262  nb3gr2nb  26267  cplgruvtxb  26292  pthdivtx  26606  pthdlem2lem  26644  crctisclwlk  26670  wwlks  26708  wspthnonp  26725  wlkiswwlks2lem1  26736  wwlksnndef  26781  clwwlksnfi  26893  clwwlksel  26894  clwwlksf1  26897  clwlksf1clwwlklem  26948  umgr3v3e3cycl  27024  frgrncvvdeq  27153  sspval  27548  blo3i  27627  ajfval  27634  spanval  28162  cmcmlem  28420  leopnmid  28967  csmdsymi  29163  chirredlem4  29222  sumdmdlem  29247  difininv  29326  iundisjf  29374  padct  29471  iundisjfi  29529  fprodex01  29545  xrpxdivcld  29617  pnfneige0  29971  rrhre  30039  esumcocn  30116  hasheuni  30121  sgon  30161  sigapildsys  30199  ddemeas  30273  dya2iocct  30316  dya2iocnrect  30317  eulerpartgbij  30408  eulerpartlemgs2  30416  coinflippv  30519  hgt750lemb  30708  bnj1136  31039  bnj1175  31046  bnj1408  31078  cvmsdisj  31226  mrsubvrs  31393  mppspstlem  31442  problem4  31536  climuzcnv  31539  dford5  31583  dfon2lem7  31668  sltval2  31783  noxp1o  31790  conway  31884  scutbdaylt  31896  imageval  32012  filnetlem2  32349  df3nandALT1  32371  lukshef-ax2  32389  arg-ax  32390  bj-andnotim  32548  bj-modalbe  32653  bj-2uplex  32985  mptsnunlem  33156  onsucuni3  33186  finixpnum  33365  fin2solem  33366  matunitlindflem2  33377  poimirlem6  33386  poimirlem7  33387  poimirlem8  33388  poimirlem18  33398  poimirlem21  33401  poimirlem22  33402  poimirlem32  33412  mblfinlem3  33419  itg2addnclem2  33433  itg2addnc  33435  bddiblnc  33451  ftc1anclem6  33461  heiborlem3  33583  ismndo2  33644  rngomndo  33705  isfld2  33775  isfldidl  33838  dmncan2  33847  oprabbi  33941  opabbi  33945  ac6s3f  33950  lsat0cv  34139  pclfinclN  35055  docavalN  36231  djavalN  36243  dochval  36459  djhval  36506  dochexmidlem8  36575  dochkr1  36586  dochkr1OLDN  36587  hdmap1fval  36905  pellexlem5  37216  rmyabs  37344  jm2.24  37349  islssfgi  37461  pwslnm  37483  dgraaub  37537  clrellem  37748  frege114d  37869  frege55lem1a  37980  frege70  38047  gneispace  38252  3impexpbicom  38505  ee3bir  38529  vk15.4j  38554  onfrALTlem2  38581  ax6e2nd  38594  dfvd1impr  38612  dfvd2impr  38649  e1bir  38675  e2bir  38678  e3bir  38786  suctrALT  38881  19.21a3con13vVD  38907  3impexpbicomVD  38912  tratrbVD  38917  ssralv2VD  38922  truniALTVD  38934  trintALTVD  38936  undif3VD  38938  onfrALTlem3VD  38943  onfrALTlem2VD  38945  onfrALTVD  38947  relopabVD  38957  ax6e2ndVD  38964  2uasbanhVD  38967  vk15.4jVD  38970  sspwimp  38974  sspwimpVD  38975  sspwimpcf  38976  sspwimpcfVD  38977  suctrALTcf  38978  suctrALTcfVD  38979  suctrALT3  38980  sspwimpALT  38981  unisnALT  38982  ax6e2ndALT  38986  isosctrlem1ALT  38990  iunconnlem2  38991  supminfxrrnmpt  39514  limsuppnflem  39742  limsupubuz  39745  cncfuni  39862  iblcncfioo  39957  stoweidlem14  39994  stoweidlem17  39997  stoweidlem35  40015  stoweidlem57  40037  stirlinglem7  40060  stirlinglem10  40063  fourierdlem54  40140  fourierdlem62  40148  fourierdlem63  40149  fourierdlem65  40151  fourierdlem73  40159  fourierdlem80  40166  fourierdlem82  40168  fourierdlem101  40187  etransclem32  40246  ioorrnopnxr  40290  subsaliuncl  40339  meadjiunlem  40445  ismeannd  40447  voliunsge0lem  40452  volmea  40454  caratheodory  40505  ovnsubaddlem2  40548  hoidmvlelem5  40576  hoiqssbllem2  40600  iinhoiicc  40651  aibandbiaiaiffb  40825  dfdfat2  40974  afvres  41015  tz6.12-afv  41016  ndmaovass  41049  el1fzopredsuc  41098  fzoopth  41100  iccpartiltu  41122  iccelpart  41133  lswn0  41144  ccatpfx  41174  evenprm2  41388  lincext1  42008
  Copyright terms: Public domain W3C validator