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

Theorem biimpri 216
Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 208. (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 212 . 2 (𝜓𝜑)
32biimpi 204 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  mpbir  219  sylibr  222  sylbir  223  sylbbr  224  sylbb1  225  sylbb2  226  syl5bir  231  syl6ibr  240  mtbi  310  pm2.54  387  sylanbr  488  sylan2br  491  pm3.11  518  orbi2i  539  pm2.31  545  simplbi2  652  dfbi  658  pm2.85  893  pm3.2an3  1232  syl3an1br  1356  syl3an2br  1357  syl3an3br  1358  had1  1532  nic-axALT  1589  speimfw  1862  sbbii  1873  ceqsexv2d  3214  eueq2  3345  ralun  3755  ssunieq  4401  ax6vsep  4706  opelxpi  5061  elsnxpOLD  5580  ordunidif  5675  unizlim  5746  funtpgOLD  5842  dffo2  6016  dff1o2  6039  resdif  6054  f1o00  6067  fvimacnvALT  6228  fvcofneq  6259  exfo  6269  ressnop0  6302  fsnunfv  6335  ovid  6652  ovidig  6653  dfwe2  6849  onminex  6875  nnsuc  6950  1stnpr  7039  2ndnpr  7040  f1stres  7057  f2ndres  7058  1st2val  7061  2nd2val  7062  frxp  7150  soxp  7153  tz7.49  7403  elixpsn  7809  domdifsn  7904  domunsncan  7921  fineqvlem  8035  unblem4  8076  ordiso2  8279  domwdom  8338  zfreg  8359  inf3lem3  8386  trcl  8463  unir1  8535  ssrankr1  8557  pm54.43lem  8684  infxpenlem  8695  ween  8717  acni3  8729  kmlem1  8831  infdif  8890  ackbij1lem1  8901  fin23lem14  9014  fin23lem32  9025  isfin1-3  9067  axcc2lem  9117  axdc3lem2  9132  ac6c4  9162  zornn0g  9186  axdclem2  9201  brdom3  9207  brdom5  9208  brdom4  9209  brdom6disj  9211  konigthlem  9245  pwcfsdom  9260  cfpwsdom  9261  alephom  9262  gruina  9495  grur1  9497  grothomex  9506  grothac  9507  nqpr  9691  axcnre  9840  axpre-sup  9845  ssxr  9957  le2tri3i  10017  muldivdir  10568  0nn0  11153  uzind4  11577  rpnnen1lem5  11649  rpnnen1lem5OLD  11655  elfz4  12160  eluzfz  12162  ssfzo12bi  12383  hashgt0elex  13001  hashxplem  13031  hashfun  13035  ishashinf  13055  ffz0iswrd  13132  wrdsymb1  13142  ccatfv0  13165  lswccats1fst  13209  ccatswrd  13253  repswfsts  13324  cshinj  13353  cshw1  13364  swrdco  13379  cotr2g  13508  xptrrel  13512  trclun  13548  resqrex  13784  pwm1geoser  14384  sumeven  14893  ndvdsadd  14917  gcdcllem1  15004  gcdcllem3  15006  lcmftp  15132  lcmfunsnlem2lem2  15135  lcmfunsnlem2  15136  lcmfun  15141  ncoprmgcdne1b  15146  coprmprod  15158  coprmproddvdslem  15159  divgcdcoprmex  15163  1idssfct  15176  prmodvdslcmf  15534  cshwrepswhash1  15592  xpsff1o  15996  initoeu2  16434  clatlem  16879  clatlubcl2  16881  clatglbcl2  16883  xpsmnd  17098  sgrp2rid2  17181  xpsgrp  17302  symg2bas  17586  symgextf  17605  gsmsymgrfix  17616  gsmsymgreqlem2  17619  pmtr3ncom  17663  odlem1  17722  gexlem1  17762  dprdfeq0  18189  gsumdixp  18377  lspcl  18742  cply1mul  19430  psgndiflemB  19709  lindfind  19915  lindsind  19916  lindsind2  19918  lindff1  19919  f1linds  19924  gsumcom3fi  19966  mat1dimscm  20041  dmatmul  20063  mdetdiag  20165  mdetunilem7  20184  mdetunilem9  20186  madurid  20210  fvmptnn04if  20414  tgcl  20525  elcls  20628  opnnei  20675  neiptopnei  20687  cnpnei  20819  cmpfii  20963  txcnp  21174  xpstps  21364  fbun  21395  isfild  21413  snfil  21419  filcon  21438  isufil2  21463  hauspwpwf1  21542  cnextcn  21622  ustfilxp  21767  ustuqtop4  21799  xpsxms  22089  xpsms  22090  rlmnvc  22249  nmoid  22287  xrsmopn  22354  xrhmeo  22483  cphsqrtcl  22715  iscmet3  22816  iundisj  23039  ioorinv  23066  plyexmo  23788  aalioulem3  23809  dvtaylp  23844  dvradcnv  23895  logtayllem  24121  logtayl  24122  logbid1  24222  logbchbase  24225  relogbcxpb  24241  logbmpt  24242  logbfval  24244  musum  24633  lgsmodeq  24783  lgsmulsqcoprm  24784  2lgs  24848  pntlem3  25014  nb3grapr  25747  nb3grapr2  25748  nb3gra2nb  25749  wlkcpr  25822  2pthlem2  25891  nvnencycllem  25936  wlkiswwlk2lem1  25984  clwwlkel  26086  clwwlkf1  26089  clwlkf1clwwlklem  26141  2wlkonotv  26169  clwlknclwlkdifs  26252  frgra0v  26285  frgra3v  26294  2pthfrgrarn  26301  2pthfrgra  26303  n4cyclfrgra  26310  frgrancvvdeqlem9  26333  frgrawopreglem3  26338  frgraregorufr0  26344  numclwwlk2lem1  26394  sspval  26765  blo3i  26846  ajfval  26853  spanval  27381  cmcmlem  27639  leopnmid  28186  csmdsymi  28382  chirredlem4  28441  sumdmdlem  28466  iundisjf  28589  rnct  28684  padct  28690  iundisjfi  28747  xrpxdivcld  28779  pnfneige0  29130  rrhre  29198  esumcocn  29274  hasheuni  29279  sgon  29319  sigapildsys  29357  ddemeas  29431  1stmbfm  29454  2ndmbfm  29455  dya2iocct  29474  dya2iocnrect  29475  eulerpartgbij  29566  eulerpartlemgs2  29574  coinflippv  29677  bnj1136  30124  bnj1175  30131  bnj1408  30163  cvmsdisj  30311  mrsubvrs  30478  mppspstlem  30527  problem4  30621  climuzcnv  30624  dfon2lem7  30743  sltval2  30858  nodenselem5  30889  imageval  31012  filnetlem2  31349  df3nandALT1  31371  lukshef-ax2  31389  arg-ax  31390  sylancl3  31543  bj-andnotim  31551  bj-modalbe  31670  bj-2uplex  32005  bj-toprntopon  32046  mptsnunlem  32163  onsucuni3  32193  finixpnum  32366  fin2solem  32367  matunitlindflem2  32378  poimirlem6  32387  poimirlem7  32388  poimirlem8  32389  poimirlem18  32399  poimirlem21  32402  poimirlem22  32403  poimirlem32  32413  mblfinlem3  32420  itg2addnclem2  32434  itg2addnc  32436  bddiblnc  32452  ftc1anclem6  32462  heiborlem3  32584  ismndo2  32645  rngomndo  32706  isfld2  32776  isfldidl  32839  dmncan2  32848  oprabbi  32942  opabbi  32946  ac6s3f  32951  lsat0cv  33140  pclfinclN  34056  docavalN  35232  djavalN  35244  dochval  35460  djhval  35507  dochexmidlem8  35576  dochkr1  35587  dochkr1OLDN  35588  hdmap1fval  35906  pellexlem5  36217  rmyabs  36345  jm2.24  36350  islssfgi  36462  pwslnm  36484  dgraaub  36539  clrellem  36750  frege114d  36871  frege55lem1a  36982  frege70  37049  gneispace  37254  3impexpbicom  37508  ee3bir  37532  vk15.4j  37557  onfrALTlem2  37584  ax6e2nd  37597  dfvd1impr  37615  dfvd2impr  37652  e1bir  37678  e2bir  37681  e3bir  37789  suctrALT  37885  19.21a3con13vVD  37911  3impexpbicomVD  37916  tratrbVD  37921  ssralv2VD  37926  truniALTVD  37938  trintALTVD  37940  undif3VD  37942  onfrALTlem3VD  37947  onfrALTlem2VD  37949  onfrALTVD  37951  relopabVD  37961  ax6e2ndVD  37968  2uasbanhVD  37971  vk15.4jVD  37974  sspwimp  37978  sspwimpVD  37979  sspwimpcf  37980  sspwimpcfVD  37981  suctrALTcf  37982  suctrALTcfVD  37983  suctrALT3  37984  sspwimpALT  37985  unisnALT  37986  ax6e2ndALT  37990  isosctrlem1ALT  37994  iunconlem2  37995  cncfuni  38575  iblcncfioo  38673  stoweidlem14  38710  stoweidlem17  38713  stoweidlem35  38731  stoweidlem57  38753  stirlinglem7  38776  stirlinglem10  38779  fourierdlem54  38856  fourierdlem62  38864  fourierdlem63  38865  fourierdlem65  38867  fourierdlem73  38875  fourierdlem80  38882  fourierdlem82  38884  fourierdlem101  38903  etransclem32  38962  ioorrnopnxr  39006  subsaliuncl  39055  meadjiunlem  39161  ismeannd  39163  voliunsge0lem  39168  volmea  39170  caratheodory  39221  ovnsubaddlem2  39264  hoidmvlelem5  39292  hoiqssbllem2  39316  iinhoiicc  39368  aibandbiaiaiffb  39514  dfdfat2  39664  afvres  39705  tz6.12-afv  39706  ndmaovass  39739  el1fzopredsuc  39752  iccpartiltu  39764  iccelpart  39775  evenprm2  39965  lswn0  40046  ccatpfx  40076  2f1fvneq  40137  fzoopth  40186  upgredg  40371  nbupgrel  40568  nbusgrvtxm1  40608  nb3gr2nb  40613  cplgruvtxb  40638  pthdivtx  40936  pthdlem2lem  40974  wwlks  41039  wspthnonp  41056  1wlkiswwlks2lem1  41067  wwlksnndef  41112  clwwlksnfi  41221  clwwlksel  41222  clwwlksf1  41225  clwlksf1clwwlklem  41276  umgr3v3e3cycl  41352  frgrncvvdeq  41481  frgr2wwlkeu  41493  frrusgrord0  41504  lincext1  42038
  Copyright terms: Public domain W3C validator