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

Theorem biimpri 230
Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 222. (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 226 . 2 (𝜓𝜑)
32biimpi 218 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208
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 209
This theorem is referenced by:  mpbir  233  sylibr  236  sylbir  237  sylbbr  238  sylbb1  239  sylbb2  240  syl5bir  245  syl6ibr  254  mtbi  324  sylnib  330  simplbi2  503  sylanbr  584  sylan2br  596  pm2.54  848  orbi2i  909  pm2.31  919  pm2.85  929  pm3.11  989  syl3an1br  1402  syl3an2br  1403  syl3an3br  1404  had1  1604  nic-axALT  1675  speimfw  1966  sbbii  2081  sb2vOLD  2097  sbbiiALT  2578  mobii  2630  mo4  2649  nfabdw  2994  r19.30  3322  ceqsexv2d  3518  eueq2  3677  ralun  4143  ssunieq  4845  ax6vsep  5179  opelxpi  5564  ordunidif  6211  unizlim  6279  dffo2  6566  dff1o2  6592  resdif  6607  f1o00  6621  fvimacnvALT  6799  fvcofneq  6831  exfo  6843  ressnop0  6887  fsnunfv  6921  ovid  7264  ovidig  7265  dfwe2  7470  onminex  7496  nnsuc  7571  1stnpr  7667  2ndnpr  7668  f1stres  7687  f2ndres  7688  1st2val  7691  2nd2val  7692  frxp  7794  soxp  7797  tz7.49  8055  elixpsn  8475  domdifsn  8574  domunsncan  8591  fineqvlem  8706  unblem4  8747  ordiso2  8953  zfreg  9033  inf3lem3  9067  trcl  9144  unir1  9216  ssrankr1  9238  djuunxp  9324  pm54.43lem  9402  infxpenlem  9413  ween  9435  acni3  9447  kmlem1  9550  infdif  9605  ackbij1lem1  9616  fin23lem32  9740  isfin1-3  9782  axdc3lem2  9847  ac6c4  9877  zornn0g  9901  axdclem2  9916  rnct  9921  brdom3  9924  brdom5  9925  brdom4  9926  brdom6disj  9928  konigthlem  9964  pwcfsdom  9979  cfpwsdom  9980  alephom  9981  gruina  10214  grur1  10216  grothomex  10225  grothac  10226  nqpr  10410  axcnre  10560  axpre-sup  10565  ssxr  10684  le2tri3i  10744  muldivdir  11307  0nn0  11887  uzind4  12281  rpnnen1lem5  12355  elfz4  12881  eluzfz  12883  ssfzo12bi  13112  hashgt0elex  13743  hashgt23el  13766  hashxplem  13775  hashfun  13779  ishashinf  13802  wrdsymb1  13881  ccatfv0  13913  lswccats1fst  13970  ccatswrd  14006  ccatpfx  14039  splfv1  14093  repswfsts  14119  cshinj  14149  swrdco  14175  cotr2g  14312  trclun  14350  resqrex  14586  pwm1geoserOLD  15201  sumeven  15712  ndvdsadd  15735  gcdcllem1  15822  gcdcllem3  15824  lcmftp  15954  lcmfunsnlem2lem2  15957  lcmfunsnlem2  15958  lcmfun  15963  coprmprod  15979  coprmproddvdslem  15980  divgcdcoprmex  15984  1idssfct  15998  prmodvdslcmf  16357  cshwrepswhash1  16411  xpsfrnel2  16812  xpsff1o  16815  initoeu2  17251  clatlem  17696  clatlubcl2  17698  clatglbcl2  17700  xpsmnd  17926  xpsgrp  18193  mulgfval  18201  gsmsymgrfix  18531  pmtr3ncom  18578  gsumcom3fi  19074  dprdfeq0  19119  gsumdixp  19334  lspcl  19720  lindfind  20932  lindsind  20933  lindsind2  20935  lindff1  20936  f1linds  20941  mat1dimscm  21056  mdetunilem7  21199  fvmptnn04if  21429  tgcl  21549  elcls  21653  opnnei  21700  neiptopnei  21712  cnpnei  21844  cmpfii  21989  txcnp  22200  xpstps  22390  fbun  22420  isfild  22438  snfil  22444  filconn  22463  isufil2  22488  hauspwpwf1  22567  cnextcn  22647  ustfilxp  22793  ustuqtop4  22825  xpsxms  23116  xpsms  23117  rlmnvc  23284  nmoid  23323  xrsmopn  23392  xrhmeo  23526  cphsqrtcl  23764  iscmet3  23872  iundisj  24127  ioorinv  24155  bddiblnc  24420  dvtaylp  24940  logbid1  25329  logbchbase  25332  relogbcxpb  25348  logbmpt  25349  logbfval  25351  musum  25751  lgsmodeq  25901  lgsmulsqcoprm  25902  2lgs  25966  2sqnn0  25997  pntlem3  26168  nbupgrel  27110  nbusgrvtxm1  27144  nb3gr2nb  27149  pthdivtx  27493  pthdlem2lem  27531  crctisclwlk  27558  wwlks  27596  wwlksonvtx  27616  wspthnonp  27620  wlkiswwlks2lem1  27630  wwlksnndef  27666  wwlksnfi  27667  clwlkclwwlkf1lem3  27766  clwlkclwwlkf1  27770  clwwlknnn  27793  clwwlkel  27806  clwwlkf1  27809  wwlksext2clwwlk  27817  clwwlknonwwlknonb  27866  umgr3v3e3cycl  27944  frgrncvvdeq  28069  sspval  28481  blo3i  28560  ajfval  28567  spanval  29091  cmcmlem  29349  leopnmid  29896  csmdsymi  30092  chirredlem4  30151  sumdmdlem  30176  iundisjf  30322  padct  30438  iundisjfi  30502  hashxpe  30512  fprodex01  30524  xrpxdivcld  30594  wrdt2ind  30610  lsmsnorb  30950  mxidlnzr  30983  extdgval  31051  ccfldextdgrr  31064  pnfneige0  31198  rrhre  31266  esumcocn  31343  hasheuni  31348  sgon  31387  sigapildsys  31425  ddemeas  31499  dya2iocct  31542  dya2iocnrect  31543  eulerpartgbij  31634  eulerpartlemgs2  31642  coinflippv  31745  signstfvneq0  31846  hgt750lemb  31931  bnj1136  32273  bnj1175  32280  bnj1408  32312  pthhashvtx  32378  spthcycl  32380  upgracycumgr  32404  umgracycusgr  32405  cvmsdisj  32521  mrsubvrs  32773  mppspstlem  32822  problem4  32915  climuzcnv  32918  dford5  32961  dfon2lem7  33038  fprlem1  33141  sltval2  33167  noxp1o  33174  conway  33268  scutbdaylt  33280  imageval  33395  filnetlem2  33731  df3nandALT1  33751  lukshef-ax2  33767  arg-ax  33768  bj-andnotim  33926  bj-modalbe  34026  bj-hbs1  34138  bj-hbsb2av  34140  bj-2uplex  34347  mptsnunlem  34632  onsucuni3  34661  fvineqsneq  34706  finixpnum  34914  fin2solem  34915  matunitlindflem2  34926  poimirlem6  34935  poimirlem7  34936  poimirlem8  34937  poimirlem18  34947  poimirlem21  34950  poimirlem22  34951  poimirlem32  34961  mblfinlem3  34968  itg2addnclem2  34981  itg2addnc  34983  ftc1anclem6  35007  heiborlem3  35123  ismndo2  35184  rngomndo  35245  isfld2  35315  isfldidl  35378  dmncan2  35387  oprabbi  35471  opabbi  35475  ac6s3f  35481  relcnveq3  35610  elrelscnveq3  35763  lsat0cv  36201  pclfinclN  37118  docavalN  38291  djavalN  38303  dochval  38519  djhval  38566  dochexmidlem8  38635  dochkr1  38646  dochkr1OLDN  38647  hdmap1fval  38964  lcmineqlem13  39189  selvval2lem5  39245  pellexlem5  39563  rmyabs  39688  jm2.24  39693  islssfgi  39805  pwslnm  39827  dgraaub  39881  ensucne0OLD  40027  iscard5  40032  clrellem  40113  frege114d  40234  frege55lem1a  40343  frege70  40410  gneispace  40615  3impexpbicom  40964  ee3bir  40988  vk15.4j  41013  onfrALTlem2  41031  ax6e2nd  41043  dfvd1impr  41061  dfvd2impr  41089  e1bir  41115  e2bir  41118  e3bir  41224  suctrALT  41311  19.21a3con13vVD  41337  3impexpbicomVD  41342  tratrbVD  41346  ssralv2VD  41351  truniALTVD  41363  trintALTVD  41365  undif3VD  41367  onfrALTlem3VD  41372  onfrALTlem2VD  41374  onfrALTVD  41376  relopabVD  41386  ax6e2ndVD  41393  2uasbanhVD  41396  vk15.4jVD  41399  sspwimp  41403  sspwimpVD  41404  sspwimpcf  41405  sspwimpcfVD  41406  suctrALTcf  41407  suctrALTcfVD  41408  suctrALT3  41409  sspwimpALT  41410  unisnALT  41411  ax6e2ndALT  41415  isosctrlem1ALT  41419  iunconnlem2  41420  supminfxrrnmpt  41897  limsuppnflem  42139  limsupubuz  42142  cncfuni  42315  iblcncfioo  42407  stoweidlem14  42443  stoweidlem17  42446  stoweidlem35  42464  stoweidlem57  42486  stirlinglem7  42509  stirlinglem10  42512  fourierdlem54  42589  fourierdlem62  42597  fourierdlem63  42598  fourierdlem65  42600  fourierdlem73  42608  fourierdlem80  42615  fourierdlem82  42617  fourierdlem101  42636  etransclem32  42695  ioorrnopnxr  42736  subsaliuncl  42785  meadjiunlem  42891  ismeannd  42893  voliunsge0lem  42898  volmea  42900  caratheodory  42954  ovnsubaddlem2  42997  hoidmvlelem5  43025  hoiqssbllem2  43049  iinhoiicc  43100  aibandbiaiaiffb  43275  funressnvmo  43424  dfdfat2  43471  afvres  43515  tz6.12-afv  43516  ndmaovass  43549  afv2res  43582  tz6.12-afv2  43583  el1fzopredsuc  43669  fzoopth  43671  fundcmpsurinjimaid  43715  iccpartiltu  43726  iccelpart  43737  lswn0  43748  ichnfimlem  43767  prprelb  43820  evenprm2  44020  lincext1  44650
  Copyright terms: Public domain W3C validator