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  311  pm2.54  388  sylanbr  491  sylan2br  494  pm3.11  521  orbi2i  542  pm2.31  548  simplbi2  656  dfbi  664  sylanblrc  700  pm2.85  934  pm3.2an3OLD  1423  syl3an1br  1509  syl3an2br  1510  syl3an3br  1511  had1  1683  nic-axALT  1740  speimfw  2034  sbbii  2045  ceqsexv2d  3375  eueq2  3513  ralun  3930  ssunieq  4616  ax6vsep  4929  opelxpi  5297  elsnxpOLD  5831  ordunidif  5926  unizlim  5997  funtpgOLD  6096  dffo2  6272  dff1o2  6295  resdif  6310  f1o00  6324  fvimacnvALT  6491  fvcofneq  6522  exfo  6532  ressnop0  6575  fsnunfv  6609  2f1fvneq  6672  ovid  6934  ovidig  6935  dfwe2  7138  onminex  7164  nnsuc  7239  1stnpr  7329  2ndnpr  7330  f1stres  7349  f2ndres  7350  1st2val  7353  2nd2val  7354  frxp  7447  soxp  7450  tz7.49  7701  elixpsn  8105  domdifsn  8200  domunsncan  8217  fineqvlem  8331  unblem4  8372  ordiso2  8577  domwdom  8636  zfreg  8657  inf3lem3  8692  trcl  8769  unir1  8841  ssrankr1  8863  pm54.43lem  9007  infxpenlem  9018  ween  9040  acni3  9052  kmlem1  9156  infdif  9215  ackbij1lem1  9226  fin23lem14  9339  fin23lem32  9350  isfin1-3  9392  axcc2lem  9442  axdc3lem2  9457  ac6c4  9487  zornn0g  9511  axdclem2  9526  rnct  9531  brdom3  9534  brdom5  9535  brdom4  9536  brdom6disj  9538  konigthlem  9574  pwcfsdom  9589  cfpwsdom  9590  alephom  9591  gruina  9824  grur1  9826  grothomex  9835  grothac  9836  nqpr  10020  axcnre  10169  axpre-sup  10174  ssxr  10291  le2tri3i  10351  muldivdir  10904  0nn0  11491  uzind4  11931  rpnnen1lem5  12003  rpnnen1lem5OLD  12009  elfz4  12520  eluzfz  12522  ssfzo12bi  12749  hashgt0elex  13373  hashxplem  13404  hashfun  13408  ishashinf  13431  ffz0iswrd  13510  wrdsymb1  13521  ccatfv0  13547  lswccats1fst  13603  ccatswrd  13648  repswfsts  13720  cshinj  13749  cshw1  13760  swrdco  13775  cotr2g  13908  xptrrel  13912  trclun  13946  resqrex  14182  pwm1geoser  14791  sumeven  15304  ndvdsadd  15328  gcdcllem1  15415  gcdcllem3  15417  lcmftp  15543  lcmfunsnlem2lem2  15546  lcmfunsnlem2  15547  lcmfun  15552  ncoprmgcdne1b  15557  coprmprod  15569  coprmproddvdslem  15570  divgcdcoprmex  15574  1idssfct  15587  prmodvdslcmf  15945  cshwrepswhash1  16003  xpsff1o  16422  initoeu2  16859  clatlem  17304  clatlubcl2  17306  clatglbcl2  17308  xpsmnd  17523  sgrp2rid2  17606  xpsgrp  17727  symgextf  18029  gsmsymgrfix  18040  gsmsymgreqlem2  18043  pmtr3ncom  18087  odlem1  18146  gexlem1  18186  dprdfeq0  18613  gsumdixp  18801  lspcl  19170  cply1mul  19858  psgndiflemB  20140  lindfind  20349  lindsind  20350  lindsind2  20352  lindff1  20353  f1linds  20358  gsumcom3fi  20400  mat1dimscm  20475  dmatmul  20497  mdetdiag  20599  mdetunilem7  20618  mdetunilem9  20620  madurid  20644  fvmptnn04if  20848  toprntopon  20923  tgcl  20967  elcls  21071  opnnei  21118  neiptopnei  21130  cnpnei  21262  cmpfii  21406  txcnp  21617  xpstps  21807  fbun  21837  isfild  21855  snfil  21861  filconn  21880  isufil2  21905  hauspwpwf1  21984  cnextcn  22064  ustfilxp  22209  ustuqtop4  22241  xpsxms  22532  xpsms  22533  rlmnvc  22700  nmoid  22739  xrsmopn  22808  xrhmeo  22938  cphsqrtcl  23176  iscmet3  23283  iundisj  23508  ioorinv  23536  plyexmo  24259  aalioulem3  24280  dvtaylp  24315  dvradcnv  24366  logtayllem  24596  logtayl  24597  logbid1  24697  logbchbase  24700  relogbcxpb  24716  logbmpt  24717  logbfval  24719  musum  25108  lgsmodeq  25258  lgsmulsqcoprm  25259  2lgs  25323  pntlem3  25489  nbupgrel  26432  nbusgrvtxm1  26471  nb3gr2nb  26476  cplgruvtxbOLD  26513  pthdivtx  26827  pthdlem2lem  26865  crctisclwlk  26892  wwlks  26930  wwlksonvtx  26952  wspthnonp  26960  wlkiswwlks2lem1  26970  wwlksnndef  27015  clwlkclwwlkf1lem3  27121  clwlkclwwlkf1  27125  clwwlknnn  27153  clwwlknfi  27166  clwwlkel  27167  clwwlkf1  27170  clwlksf1clwwlklemOLD  27214  clwwlknonwwlknonb  27246  umgr3v3e3cycl  27328  frgrncvvdeq  27455  sspval  27879  blo3i  27958  ajfval  27965  spanval  28493  cmcmlem  28751  leopnmid  29298  csmdsymi  29494  chirredlem4  29553  sumdmdlem  29578  difininv  29653  iundisjf  29701  padct  29798  iundisjfi  29856  fprodex01  29872  xrpxdivcld  29944  pnfneige0  30298  rrhre  30366  esumcocn  30443  hasheuni  30448  sgon  30488  sigapildsys  30526  ddemeas  30600  dya2iocct  30643  dya2iocnrect  30644  eulerpartgbij  30735  eulerpartlemgs2  30743  coinflippv  30846  hgt750lemb  31035  bnj1136  31364  bnj1175  31371  bnj1408  31403  cvmsdisj  31551  mrsubvrs  31718  mppspstlem  31767  problem4  31861  climuzcnv  31864  dford5  31907  dfon2lem7  31991  sltval2  32107  noxp1o  32114  conway  32208  scutbdaylt  32220  imageval  32335  filnetlem2  32672  df3nandALT1  32694  lukshef-ax2  32712  arg-ax  32713  bj-andnotim  32871  bj-modalbe  32976  bj-2uplex  33308  mptsnunlem  33488  onsucuni3  33518  finixpnum  33699  fin2solem  33700  matunitlindflem2  33711  poimirlem6  33720  poimirlem7  33721  poimirlem8  33722  poimirlem18  33732  poimirlem21  33735  poimirlem22  33736  poimirlem32  33746  mblfinlem3  33753  itg2addnclem2  33767  itg2addnc  33769  bddiblnc  33785  ftc1anclem6  33795  heiborlem3  33917  ismndo2  33978  rngomndo  34039  isfld2  34109  isfldidl  34172  dmncan2  34181  oprabbi  34275  opabbi  34279  ac6s3f  34284  relcnveq3  34408  elrelscnveq3  34556  lsat0cv  34815  pclfinclN  35731  docavalN  36906  djavalN  36918  dochval  37134  djhval  37181  dochexmidlem8  37250  dochkr1  37261  dochkr1OLDN  37262  hdmap1fval  37580  pellexlem5  37891  rmyabs  38019  jm2.24  38024  islssfgi  38136  pwslnm  38158  dgraaub  38212  clrellem  38423  frege114d  38544  frege55lem1a  38654  frege70  38721  gneispace  38926  3impexpbicom  39179  ee3bir  39203  vk15.4j  39228  onfrALTlem2  39255  ax6e2nd  39268  dfvd1impr  39286  dfvd2impr  39323  e1bir  39349  e2bir  39352  e3bir  39460  suctrALT  39552  19.21a3con13vVD  39578  3impexpbicomVD  39583  tratrbVD  39588  ssralv2VD  39593  truniALTVD  39605  trintALTVD  39607  undif3VD  39609  onfrALTlem3VD  39614  onfrALTlem2VD  39616  onfrALTVD  39618  relopabVD  39628  ax6e2ndVD  39635  2uasbanhVD  39638  vk15.4jVD  39641  sspwimp  39645  sspwimpVD  39646  sspwimpcf  39647  sspwimpcfVD  39648  suctrALTcf  39649  suctrALTcfVD  39650  suctrALT3  39651  sspwimpALT  39652  unisnALT  39653  ax6e2ndALT  39657  isosctrlem1ALT  39661  iunconnlem2  39662  supminfxrrnmpt  40191  limsuppnflem  40437  limsupubuz  40440  cncfuni  40594  iblcncfioo  40689  stoweidlem14  40726  stoweidlem17  40729  stoweidlem35  40747  stoweidlem57  40769  stirlinglem7  40792  stirlinglem10  40795  fourierdlem54  40872  fourierdlem62  40880  fourierdlem63  40881  fourierdlem65  40883  fourierdlem73  40891  fourierdlem80  40898  fourierdlem82  40900  fourierdlem101  40919  etransclem32  40978  ioorrnopnxr  41022  subsaliuncl  41071  meadjiunlem  41177  ismeannd  41179  voliunsge0lem  41184  volmea  41186  caratheodory  41240  ovnsubaddlem2  41283  hoidmvlelem5  41311  hoiqssbllem2  41335  iinhoiicc  41386  aibandbiaiaiffb  41560  dfdfat2  41709  afvres  41750  tz6.12-afv  41751  ndmaovass  41784  el1fzopredsuc  41837  fzoopth  41839  iccpartiltu  41860  iccelpart  41871  lswn0  41882  ccatpfx  41911  evenprm2  42125  lincext1  42745
  Copyright terms: Public domain W3C validator