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  1826  sbbii  1837  exmidne  2696  ceqsexv2d  3120  eueq2  3251  ralun  3661  ssunieq  4306  ax6vsep  4611  opelxpi  4966  ndmima  5312  elsnxpOLD  5485  ordunidif  5580  unizlim  5651  funtpgOLD  5747  dffo2  5921  dff1o2  5944  resdif  5959  f1o00  5972  fvimacnvALT  6133  fvcofneq  6164  exfo  6174  ressnop0  6207  fsnunfv  6240  ovid  6557  ovidig  6558  dfwe2  6754  onminex  6780  nnsuc  6855  1stnpr  6943  2ndnpr  6944  f1stres  6961  f2ndres  6962  1st2val  6965  2nd2val  6966  frxp  7054  soxp  7057  tz7.49  7307  elixpsn  7713  domdifsn  7808  domunsncan  7825  fineqvlem  7939  unblem4  7980  ordiso2  8183  domwdom  8242  zfreg  8263  inf3lem3  8290  trcl  8367  unir1  8439  ssrankr1  8461  pm54.43lem  8588  infxpenlem  8599  ween  8621  acni3  8633  kmlem1  8735  infdif  8794  ackbij1lem1  8805  fin23lem14  8918  fin23lem32  8929  isfin1-3  8971  axcc2lem  9021  axdc3lem2  9036  ac6c4  9066  zornn0g  9090  axdclem2  9105  brdom3  9111  brdom5  9112  brdom4  9113  brdom6disj  9115  konigthlem  9149  pwcfsdom  9164  cfpwsdom  9165  alephom  9166  gruina  9399  grur1  9401  grothomex  9410  grothac  9411  nqpr  9595  axcnre  9744  axpre-sup  9749  ssxr  9861  le2tri3i  9922  muldivdir  10473  0nn0  11066  uzind4  11490  rpnnen1lem5  11564  rpnnen1lem5OLD  11570  elfz4  12078  eluzfz  12080  ssfzo12bi  12301  hashgt0elex  12919  hashxplem  12949  hashfun  12953  ishashinf  12973  ffz0iswrd  13050  wrdsymb1  13060  ccatfv0  13083  lswccats1fst  13127  ccatswrd  13171  repswfsts  13242  cshinj  13271  cshw1  13282  swrdco  13297  cotr2g  13426  xptrrel  13430  trclun  13466  resqrex  13702  pwm1geoser  14312  sumeven  14821  ndvdsadd  14848  gcdcllem1  14936  gcdcllem3  14938  lcmftp  15067  lcmfunsnlem2lem2  15070  lcmfunsnlem2  15071  lcmfun  15076  ncoprmgcdne1b  15081  coprmprod  15093  coprmproddvdslem  15094  divgcdcoprmex  15098  1idssfct  15111  prmodvdslcmf  15477  cshwrepswhash1  15535  xpsff1o  15947  initoeu2  16385  clatlem  16830  clatlubcl2  16832  clatglbcl2  16834  xpsmnd  17049  sgrp2rid2  17132  xpsgrp  17253  symg2bas  17537  symgextf  17556  gsmsymgrfix  17567  gsmsymgreqlem2  17570  pmtr3ncom  17614  odlem1  17679  odlem1OLD  17682  gexlem1  17726  gexlem1OLD  17728  dprdfeq0  18155  gsumdixp  18343  lspcl  18705  cply1mul  19393  psgndiflemB  19675  lindfind  19881  lindsind  19882  lindsind2  19884  lindff1  19885  f1linds  19890  gsumcom3fi  19932  mat1dimscm  20007  dmatmul  20029  mdetdiag  20131  mdetunilem7  20150  mdetunilem9  20152  madurid  20176  fvmptnn04if  20380  tgcl  20491  elcls  20594  opnnei  20641  neiptopnei  20653  cnpnei  20785  cmpfii  20929  txcnp  21140  xpstps  21330  fbun  21361  isfild  21379  snfil  21385  filcon  21404  isufil2  21429  hauspwpwf1  21508  cnextcn  21588  ustfilxp  21733  ustuqtop4  21765  xpsxms  22055  xpsms  22056  rlmnvc  22211  nmoid  22269  xrsmopn  22336  xrhmeo  22480  cphsqrtcl  22666  iscmet3  22767  iundisj  23002  ioorinv  23029  plyexmo  23760  aalioulem3  23784  dvtaylp  23819  dvradcnv  23870  logtayllem  24096  logtayl  24097  logbid1  24197  logbchbase  24200  relogbcxpb  24216  logbmpt  24217  logbfval  24219  musum  24610  lgsmodeq  24760  lgsmulsqcoprm  24761  2lgs  24825  pntlem3  24991  nb3grapr  25724  nb3grapr2  25725  nb3gra2nb  25726  wlkcpr  25799  2pthlem2  25868  nvnencycllem  25913  wlkiswwlk2lem1  25961  clwwlkel  26063  clwwlkf1  26066  clwlkf1clwwlklem  26118  2wlkonotv  26146  clwlknclwlkdifs  26229  frgra0v  26262  frgra3v  26271  2pthfrgrarn  26278  2pthfrgra  26280  n4cyclfrgra  26287  frgrancvvdeqlem9  26310  frgrawopreglem3  26315  frgraregorufr0  26321  numclwwlk2lem1  26371  sspval  26742  blo3i  26823  ajfval  26830  spanval  27368  cmcmlem  27626  leopnmid  28173  csmdsymi  28369  chirredlem4  28428  sumdmdlem  28453  iundisjf  28576  rnct  28671  padct  28677  xrge0infssOLD  28710  iundisjfi  28741  xrpxdivcld  28773  pnfneige0  29125  rrhre  29193  esumcocn  29269  hasheuni  29274  sgon  29314  sigapildsys  29352  ddemeas  29426  1stmbfm  29449  2ndmbfm  29450  dya2iocct  29469  dya2iocnrect  29470  eulerpartgbij  29572  eulerpartlemgs2  29580  coinflippv  29683  bnj1136  30168  bnj1175  30175  bnj1408  30207  cvmsdisj  30355  mrsubvrs  30522  mppspstlem  30571  problem4  30663  climuzcnv  30666  dfon2lem7  30784  sltval2  30892  nodenselem5  30923  imageval  31046  filnetlem2  31382  df3nandALT1  31404  lukshef-ax2  31422  arg-ax  31423  sylancl3  31576  bj-andnotim  31584  bj-modalbe  31703  bj-2uplex  32038  bj-toprntopon  32079  mptsnunlem  32196  onsucuni3  32226  finixpnum  32458  fin2solem  32459  matunitlindflem2  32470  poimirlem6  32479  poimirlem7  32480  poimirlem8  32481  poimirlem18  32491  poimirlem21  32494  poimirlem22  32495  poimirlem32  32505  mblfinlem3  32512  itg2addnclem2  32526  itg2addnc  32528  bddiblnc  32544  ftc1anclem6  32554  heiborlem3  32676  ismndo2  32737  rngomndo  32798  isfld2  32868  isfldidl  32931  dmncan2  32940  oprabbi  33034  opabbi  33038  ac6s3f  33043  lsat0cv  33232  pclfinclN  34148  docavalN  35324  djavalN  35336  dochval  35552  djhval  35599  dochexmidlem8  35668  dochkr1  35679  dochkr1OLDN  35680  hdmap1fval  35998  pellexlem5  36309  rmyabs  36437  jm2.24  36442  islssfgi  36554  pwslnm  36576  dgraaub  36637  dgraaubOLD  36638  clrellem  36849  frege114d  36970  frege55lem1a  37081  frege70  37148  gneispace  37353  3impexpbicom  37607  ee3bir  37631  vk15.4j  37656  onfrALTlem2  37683  ax6e2nd  37696  dfvd1impr  37714  dfvd2impr  37751  e1bir  37777  e2bir  37780  e3bir  37888  suctrALT  37984  19.21a3con13vVD  38010  3impexpbicomVD  38015  tratrbVD  38020  ssralv2VD  38025  truniALTVD  38037  trintALTVD  38039  undif3VD  38041  onfrALTlem3VD  38046  onfrALTlem2VD  38048  onfrALTVD  38050  relopabVD  38060  ax6e2ndVD  38067  2uasbanhVD  38070  vk15.4jVD  38073  sspwimp  38077  sspwimpVD  38078  sspwimpcf  38079  sspwimpcfVD  38080  suctrALTcf  38081  suctrALTcfVD  38082  suctrALT3  38083  sspwimpALT  38084  unisnALT  38085  ax6e2ndALT  38089  isosctrlem1ALT  38093  iunconlem2  38094  cncfuni  38676  iblcncfioo  38777  stoweidlem14  38814  stoweidlem17  38817  stoweidlem35  38835  stoweidlem57  38857  stirlinglem7  38880  stirlinglem10  38883  fourierdlem54  38962  fourierdlem62  38970  fourierdlem63  38971  fourierdlem65  38973  fourierdlem73  38981  fourierdlem80  38988  fourierdlem82  38990  fourierdlem101  39009  etransclem32  39069  ioorrnopnxr  39114  subsaliuncl  39163  meadjiunlem  39269  ismeannd  39271  voliunsge0lem  39276  volmea  39278  caratheodory  39329  ovnsubaddlem2  39372  hoidmvlelem5  39400  hoiqssbllem2  39424  iinhoiicc  39476  aibandbiaiaiffb  39622  dfdfat2  39772  afvres  39813  tz6.12-afv  39814  ndmaovass  39847  el1fzopredsuc  39860  iccpartiltu  39872  iccelpart  39883  evenprm2  40073  lswn0  40154  ccatpfx  40184  2f1fvneq  40245  fzoopth  40294  upgredg  40479  nbupgrel  40676  nbusgrvtxm1  40716  nb3gr2nb  40721  cplgruvtxb  40746  pthdivtx  41044  pthdlem2lem  41082  wwlks  41147  wspthnonp  41164  1wlkiswwlks2lem1  41175  wwlksnndef  41220  clwwlksnfi  41329  clwwlksel  41330  clwwlksf1  41333  clwlksf1clwwlklem  41384  umgr3v3e3cycl  41460  frgrncvvdeq  41589  frgr2wwlkeu  41601  frrusgrord0  41612  lincext1  42146
  Copyright terms: Public domain W3C validator