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

Theorem biimpri 213
Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 205. (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 209 . 2 (𝜓𝜑)
32biimpi 201 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191
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 192
This theorem is referenced by:  mpbir  216  sylibr  219  sylbir  220  sylbbr  221  sylbb1  222  sylbb2  223  syl5bir  228  syl6ibr  237  mtbi  307  pm2.54  383  sylanbr  483  sylan2br  486  pm3.11  513  orbi2i  534  pm2.31  540  simplbi2  644  dfbi  650  pm2.85  884  pm3.2an3  1223  syl3an1br  1347  syl3an2br  1348  syl3an3br  1349  had1  1530  nic-axALT  1587  speimfw  1824  sbbii  1835  exmidne  2687  ceqsexv2d  3106  eueq2  3236  ralun  3643  ssunieq  4262  ax6vsep  4562  opelxpi  4912  ndmima  5255  ndmimaOLD  5256  elsnxp  5429  sspred  5439  ordunidif  5522  unizlim  5590  funtpg  5684  dffo2  5856  dff1o2  5879  resdif  5894  f1o00  5907  fvimacnvALT  6068  fvcofneq  6097  exfo  6107  ressnop0  6139  fsnunfv  6172  ovid  6488  ovidig  6489  dfwe2  6685  onminex  6711  nnsuc  6786  1stnpr  6874  2ndnpr  6875  f1stres  6892  f2ndres  6893  1st2val  6896  2nd2val  6897  frxp  6985  soxp  6988  tz7.49  7239  elixpsn  7644  domdifsn  7739  domunsncan  7756  fineqvlem  7870  unblem4  7911  ordiso2  8113  domwdom  8172  zfreg  8193  inf3lem3  8220  trcl  8297  unir1  8369  ssrankr1  8391  pm54.43lem  8518  infxpenlem  8529  ween  8551  acni3  8563  kmlem1  8665  infdif  8724  ackbij1lem1  8735  fin23lem14  8848  fin23lem32  8859  isfin1-3  8901  axcc2lem  8951  axdc3lem2  8966  ac6c4  8996  zornn0g  9020  axdclem2  9035  brdom3  9041  brdom5  9042  brdom4  9043  brdom6disj  9045  konigthlem  9078  pwcfsdom  9093  cfpwsdom  9094  alephom  9095  gruina  9328  grur1  9330  grothomex  9339  grothac  9340  nqpr  9524  axcnre  9673  axpre-sup  9678  ssxr  9788  le2tri3i  9849  0nn0  10975  uzind4  11307  rpnnen1lem5  11385  elfz4  11889  eluzfz  11891  ssfzo12bi  12110  hashgt0elex  12696  hashxplem  12725  hashfun  12729  ishashinf  12749  ffz0iswrd  12826  wrdsymb1  12836  ccatfv0  12859  lswccats1fst  12902  ccatswrd  12946  repswfsts  13017  cshinj  13046  cshw1  13057  swrdco  13072  cotr2g  13198  xptrrel  13202  trclun  13238  resqrex  13474  ndvdsadd  14551  gcdcllem1  14635  gcdcllem3  14637  lcmftp  14771  lcmfunsnlem2lem2  14774  lcmfunsnlem2  14775  lcmfun  14780  1idssfct  14792  ncoprmgcdne1b  14817  coprmprod  14840  coprmproddvdslem  14841  prmodvdslcmf  15167  prmordvdslcmfOLD  15181  prmordvdslcmsOLDOLD  15183  cshwrepswhash1  15234  xpsff1o  15639  initoeu2  16077  clatlem  16522  clatlubcl2  16524  clatglbcl2  16526  xpsmnd  16737  sgrp2rid2  16820  xpsgrp  16965  symg2bas  17200  symgextf  17219  gsmsymgrfix  17230  gsmsymgreqlem2  17233  pmtr3ncom  17277  odlem1  17342  odlem1OLD  17345  gexlem1  17389  gexlem1OLD  17391  dprdfeq0  17815  gsumdixp  17997  lspcl  18359  cply1mul  19046  psgndiflemB  19326  lindfind  19532  lindsind  19533  lindsind2  19535  lindff1  19536  f1linds  19541  gsumcom3fi  19583  mat1dimscm  19658  dmatmul  19680  mdetdiag  19782  mdetunilem7  19801  mdetunilem9  19803  madurid  19827  fvmptnn04if  20031  tgcl  20142  elcls  20246  opnnei  20293  neiptopnei  20305  cnpnei  20437  cmpfii  20581  txcnp  20792  xpstps  20982  fbun  21013  isfild  21031  snfil  21037  filcon  21056  isufil2  21081  hauspwpwf1  21160  cnextcn  21240  ustfilxp  21385  ustuqtop4  21417  xpsxms  21707  xpsms  21708  rlmnvc  21863  nmoid  21921  xrsmopn  21988  xrhmeo  22132  cphsqrtcl  22321  iscmet3  22422  iundisj  22661  ioorinv  22688  ioorinvOLD  22693  plyexmo  23427  aalioulem3  23451  dvtaylp  23486  dvradcnv  23537  logtayllem  23765  logtayl  23766  logbid1  23866  logbchbase  23869  relogbcxpb  23885  logbmpt  23886  logbfval  23888  musum  24281  pntlem3  24608  nb3grapr  25342  nb3grapr2  25343  nb3gra2nb  25344  wlkcpr  25418  2pthlem2  25487  nvnencycllem  25532  wlkiswwlk2lem1  25580  clwwlkel  25682  clwwlkf1  25685  clwlkf1clwwlklem  25737  2wlkonotv  25765  clwlknclwlkdifs  25848  frgra0v  25881  frgra3v  25890  2pthfrgrarn  25897  2pthfrgra  25899  n4cyclfrgra  25906  frgrancvvdeqlem9  25929  frgrawopreglem3  25934  frgraregorufr0  25940  numclwwlk2lem1  25990  subgoablo  26202  ismndo2  26236  rngomndo  26312  sspval  26525  blo3i  26606  ajfval  26613  spanval  27149  cmcmlem  27407  leopnmid  27954  csmdsymi  28150  chirredlem4  28209  sumdmdlem  28234  iundisjf  28358  rnct  28456  padct  28463  xrge0infssOLD  28497  iundisjfi  28528  xrpxdivcld  28560  pnfneige0  28912  rrhre  28980  esumcocn  29056  hasheuni  29061  sgon  29101  sigapildsys  29139  ddemeas  29213  1stmbfm  29236  2ndmbfm  29237  dya2iocct  29256  dya2iocnrect  29257  eulerpartgbij  29359  eulerpartlemgs2  29367  coinflippv  29470  bnj1136  29958  bnj1175  29965  bnj1408  29997  cvmsdisj  30145  mrsubvrs  30312  mppspstlem  30361  problem4  30452  climuzcnv  30467  dfon2lem7  30586  sltval2  30694  nodenselem5  30725  imageval  30848  filnetlem2  31184  df3nandALT1  31206  lukshef-ax2  31224  arg-ax  31225  sylancl3  31348  bj-andnotim  31356  bj-modalbe  31466  bj-2uplex  31802  bj-toprntopon  31843  mptsnunlem  31961  onsucuni3  31991  finixpnum  32163  fin2solem  32164  matunitlindflem2  32175  poimirlem6  32184  poimirlem7  32185  poimirlem8  32186  poimirlem18  32196  poimirlem21  32199  poimirlem22  32200  poimirlem32  32210  mblfinlem3  32217  itg2addnclem2  32232  itg2addnc  32234  bddiblnc  32250  ftc1anclem6  32260  heiborlem3  32382  isfld2  32475  isfldidl  32538  dmncan2  32547  oprabbi  32641  opabbi  32645  ac6s3f  32650  lsat0cv  32839  pclfinclN  33755  docavalN  34931  djavalN  34943  dochval  35159  djhval  35206  dochexmidlem8  35275  dochkr1  35286  dochkr1OLDN  35287  hdmap1fval  35605  pellexlem5  35917  rmyabs  36048  jm2.24  36053  islssfgi  36170  pwslnm  36192  dgraaub  36253  dgraaubOLD  36254  clrellem  36468  frege114d  36589  frege55lem1a  36701  frege70  36768  gneispace  36930  3impexpbicom  37191  ee3bir  37215  vk15.4j  37241  onfrALTlem2  37268  ax6e2nd  37281  dfvd1impr  37299  dfvd2impr  37336  e1bir  37362  e2bir  37365  e3bir  37474  suctrALT  37570  19.21a3con13vVD  37596  3impexpbicomVD  37601  tratrbVD  37606  ssralv2VD  37611  truniALTVD  37623  trintALTVD  37625  undif3VD  37627  onfrALTlem3VD  37632  onfrALTlem2VD  37634  onfrALTVD  37636  relopabVD  37646  ax6e2ndVD  37653  2uasbanhVD  37656  vk15.4jVD  37659  sspwimp  37663  sspwimpVD  37664  sspwimpcf  37665  sspwimpcfVD  37666  suctrALTcf  37667  suctrALTcfVD  37668  suctrALT3  37669  sspwimpALT  37670  unisnALT  37671  ax6e2ndALT  37675  isosctrlem1ALT  37679  iunconlem2  37680  infrglbOLD  38071  cncfuni  38173  iblcncfioo  38274  stoweidlem14  38310  stoweidlem17  38313  stoweidlem35  38332  stoweidlem57  38354  stirlinglem7  38378  stirlinglem10  38381  fourierdlem54  38460  fourierdlem62  38468  fourierdlem63  38469  fourierdlem65  38471  fourierdlem73  38479  fourierdlem80  38486  fourierdlem82  38488  fourierdlem101  38507  etransclem32  38567  ioorrnopnxr  38612  meadjiunlem  38753  ismeannd  38755  voliunsge0lem  38760  volmea  38762  caratheodory  38813  ovnsubaddlem2  38856  hoidmvlelem5  38884  hoiqssbllem2  38908  iinhoiicc  38960  aibandbiaiaiffb  39003  dfdfat2  39153  afvres  39194  tz6.12-afv  39195  ndmaovass  39228  el1fzopredsuc  39242  iccpartiltu  39256  iccelpart  39267  evenprm2  39362  lswn0  39442  ccatpfx  39472  2f1fvneq  39533  fzoopth  39585  upgredg  39770  nbupgrel  39967  nbusgrvtxm1  40007  nb3gr2nb  40012  cplgruvtxb  40037  pthdivtx  40335  pthdlem2lem  40373  wwlks  40438  wspthnonp  40455  1wlkiswwlks2lem1  40466  wwlksnndef  40511  clwwlksnfi  40620  clwwlksel  40621  clwwlksf1  40624  clwlksf1clwwlklem  40675  umgr3v3e3cycl  40751  frgrncvvdeq  40880  frgr2wwlkeu  40892  frrusgrord0  40903  lincext1  41437
  Copyright terms: Public domain W3C validator