MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpi Unicode version

Theorem biimpi 194
Description: Infer an implication from a logical equivalence. (Contributed by NM, 29-Dec-1992.)
Hypothesis
Ref Expression
biimpi.1
Assertion
Ref Expression
biimpi

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2
2 bi1 186 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  sylbi  195  sylib  196  sylbb  197  biimpri  206  mpbi  208  syl5bi  217  syl6ib  226  syl7bi  230  syl8ib  231  pm2.53  373  simplbi  460  simprbi  464  sylanb  472  sylan2b  475  pm3.1  498  orbi2i  519  pm2.32  526  anc2l  555  pm3.37  579  dfbi  629  pm2.76  848  pm5.15  889  pm5.16  890  pm5.75  937  rnlemOLD  965  simp1bi  1011  simp2bi  1012  simp3bi  1013  syl3an1b  1264  syl3an2b  1265  syl3an3b  1266  nic-ax  1506  19.25  1691  stdpc5v  1732  sbbii  1746  spvw  1756  excomim  1850  stdpc5  1908  sb9i  2170  axc11n-16  2268  exmoeu  2316  2mo  2373  2moOLD  2374  eqeq1d  2459  eqeq1OLD  2462  eleq2OLD  2532  gencbvex  3153  moeq  3275  euind  3286  reuind  3303  eqsbc3r  3389  ra4v  3423  ra4  3425  ssel  3497  unssd  3679  ssind  3721  n0moeu  3798  ss0  3816  uneqdifeq  3916  rabsnif  4099  prprc  4142  ssunsn2  4189  eqsn  4191  unisn2  4588  snexALT  4638  reusv3i  4659  snex  4693  brrelex12  5042  elrel  5110  exopxfr2  5152  dmxp  5226  xpssres  5313  elres  5314  elimasni  5369  xpdifid  5440  dmsnsnsn  5491  coi2  5529  xpco  5552  iotabi  5565  uniabio  5566  iotaint  5569  nfunv  5624  funun  5635  funcnv3  5654  funimass1  5666  funssxp  5749  f0dom0  5774  f1o00  5853  dffv3  5867  dffv2  5946  fndmin  5994  iinpreima  6017  fveqressseq  6027  fsn2  6071  ftpg  6081  fnsuppeq0OLD  6132  f12dfv  6179  f13dfv  6180  nvocnv  6187  isoselem  6237  riotaxfrd  6288  oprabid  6323  mpt2difsnif  6395  ovima0  6454  sorpsscmpl  6591  unexg  6601  ordsson  6625  peano2  6720  1stval  6802  2ndval  6803  1stdm  6847  oprabco  6884  f1o2ndf1  6908  poxp  6912  suppval1  6924  funsssuppss  6945  fnsuppeq0  6947  imacosupp  6959  tz7.49c  7130  undifixp  7525  bren2  7566  ensym  7584  en1uniel  7607  domunsn  7687  limenpsi  7712  php4  7724  snnen2o  7726  isinf  7753  en2  7776  findcard2  7780  unfilem1  7804  suppssfifsupp  7864  fsuppunbi  7870  elfiun  7910  marypha1lem  7913  marypha2lem3  7917  supval2  7935  supmaxlemOLD  7945  brwdom2  8020  brwdom3  8029  sucprcreg  8046  preleq  8055  tcmin  8193  prwf  8250  r1pw  8284  rankuni2b  8292  rankr1id  8301  cardval3  8354  ficardom  8363  cardmin2  8400  isinfcard  8494  iscard3  8495  alephval3  8512  dfac9  8537  kmlem6  8556  ackbij1lem12  8632  fin23lem29  8742  fin23lem30  8743  fin23lem41  8753  isf32lem11  8764  isfin1-3  8787  fin1a2lem11  8811  fin1a2lem12  8812  fin1a2lem13  8813  axcc2lem  8837  dominf  8846  axdc4lem  8856  dominfac  8969  pwcfsdom  8979  cfpwsdom  8980  tskuni  9182  wfgru  9215  rpregt0  11262  supxrun  11536  elfz1end  11744  1fv  11821  elfzonlteqm1  11891  fzennn  12078  cardfz  12080  fsuppmapnn0fiubex  12098  fsuppmapnn0fiub0  12099  ser0  12159  crreczi  12291  faclbnd  12368  bcn1  12391  hashrabsn01  12441  hashge0  12455  hashssdif  12475  hashsnlei  12478  hashpw  12494  hash2prd  12518  swrd0len0  12660  swrdtrcfv  12668  swrdswrd  12685  swrdccatwrd  12693  swrdccatin2  12712  swrdccat3  12717  swrdccat3a  12719  repsundef  12743  cshwlen  12770  s4f1o  12866  sqrt0  13075  cau3lem  13187  harmonic  13670  mertenslem2  13694  prodf1  13700  fprodfac  13777  rpnnen2  13959  prmind2  14228  pceq0  14394  prmreclem6  14439  0ram  14538  ram0  14540  cshwsdisj  14583  cshwsiun  14584  ressbas2  14688  ressinbas  14693  mrcuni  15018  mreexexlem4d  15044  catpropd  15104  arwhoma  15372  joinfval  15631  meetfval  15645  clatlem  15741  lubun  15753  psssdm  15846  ismgmn0  15874  plusfeq  15879  isnsgrp  15915  isnmnd  15924  grpissubg  16221  idrespermg  16436  symgextfv  16443  fvcosymgeq  16454  pmtrprfv3  16479  pmtr3ncomlem1  16498  psgnunilem4  16522  gsummptfzsplitl  16953  gsumzoppg  16967  gsum2dlem1  16997  gsum2dlem2  16998  gsum2d  16999  gsum2dOLD  17000  srg1zr  17180  staffn  17498  scafeq  17532  lbsexg  17810  lidldvgen  17903  ply1bascl2  18243  cply1mul  18335  lply1binom  18348  prmirred  18525  prmirredOLD  18528  zlmassa  18561  frgpcyg  18612  ipfeq  18685  dsmmbas2  18768  frlmbas3  18807  mamufacex  18891  matsubgcell  18936  matinvgcell  18937  matvscacell  18938  mpt2matmul  18948  matepmcl  18964  matepm2cl  18965  mat1dimbas  18974  scmatscm  19015  smatvscl  19026  marrepcl  19066  marepvcl  19071  mulmarep1el  19074  mulmarep1gsum1  19075  mulmarep1gsum2  19076  submabas  19080  nfimdetndef  19091  mdetfval1  19092  m1detdiag  19099  mdetdiag  19101  mdetunilem7  19120  mdetunilem9  19122  m2detleib  19133  gsummatr01lem3  19159  smadiadetlem4  19171  slesolinv  19182  slesolinvbi  19183  slesolex  19184  cramerimplem2  19186  pmatcoe1fsupp  19202  mat2pmatbas  19227  mat2pmatmul  19232  mat2pmatlin  19236  m2cpminvid2lem  19255  decpmatmul  19273  monmatcollpw  19280  pmatcollpw3fi  19286  pm2mpf1  19300  pm2mpghm  19317  fvmptnn04ifb  19352  cayhamlem1  19367  isbasis3g  19450  isopn2  19533  ntrval2  19552  toponmre  19594  innei  19626  restcld  19673  restcldi  19674  neitr  19681  discmp  19898  cmpsublem  19899  cmpsub  19900  2ndcctbss  19956  ssref  20013  lfinun  20026  dissnref  20029  ptcnp  20123  imasnopn  20191  imasncld  20192  imasncls  20193  kqf  20248  fbun  20341  opnfbas  20343  supfil  20396  ufprim  20410  acufl  20418  filufint  20421  ufldom  20463  hausflf2  20499  alexsubALTlem4  20550  cnextfval  20562  cnextfun  20564  cnextfres  20568  trust  20732  utoptop  20737  ustuqtop1  20744  metustidOLD  21062  metustid  21063  metustfbasOLD  21068  metustfbas  21069  cfilucfilOLD  21072  cfilucfil  21073  metustblOLD  21083  metustbl  21084  restmetu  21090  zlmclm  21595  cphassr  21658  ovolun  21910  volun  21955  vitalilem2  22018  dvmptfsum  22376  rolle  22391  ulmcaulem  22789  logfac  22985  logno1  23017  logreclem  23150  leibpilem1  23271  prmorcht  23452  pclogsum  23490  2sqlem10  23649  chto1lb  23663  tgldimor  23893  axcontlem7  24273  usgraop  24350  ausisusgra  24355  usgra2edg1  24383  usgrarnedg  24384  usgraedg4  24387  usgra1v  24390  usgraidx2vlem2  24392  usgraidx2v  24393  usgrares1  24410  nbgrassvwo  24437  nbgrassvwo2  24438  nb3graprlem2  24452  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  cusgra3v  24464  cusgrafilem2  24480  usgrasscusgra  24483  uvtxnbgra  24493  uvtxnb  24497  2trllemH  24554  2trllemE  24555  constr1trl  24590  usgra2adedgwlkonALT  24616  usgra2wlkspthlem2  24620  fargshiftfo  24638  wwlknndef  24737  wwlkextproplem3  24743  clwlkswlks  24758  clwwlknndef  24773  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem1  24787  clwwlkf  24794  clwwlkvbij  24801  wwlkext2clwwlk  24803  clwwnisshclwwn  24809  erclwwlkref  24813  erclwwlknref  24825  erclwwlknsym  24826  erclwwlkntr  24827  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlkfoclwwlk  24845  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  vdgrnn0pnf  24909  clwlknclwlkdifs  24960  eupatrl  24968  frgra3v  25002  3vfriswmgra  25005  1to3vfriswmgra  25007  1to3vfriendship  25008  2pthfrgra  25011  4cycl2v2nb  25016  n4cyclfrgra  25018  frgranbnb  25020  frgrancvvdeqlem4  25033  frgrawopreg  25049  frg2woteqm  25059  usg2spot2nb  25065  numclwwlkovf2ex  25086  numclwwlk3lem  25108  grpoidinvlem3  25208  nmlno0lem  25708  blocni  25720  pythi  25765  normpythi  26059  shmodsi  26307  omlsilem  26320  pjchi  26350  chlubii  26390  osumi  26560  nmlnop0iALT  26914  cnlnssadj  26999  nmopcoi  27014  mdbr3  27216  mdbr4  27217  ssmd1  27230  dmdsl3  27234  mdslmd1lem2  27245  mdslmd4i  27252  mdexchi  27254  atssma  27297  atoml2i  27302  chirredlem3  27311  mdsymlem1  27322  mdsymlem3  27324  dmdbr6ati  27342  dmdbr7ati  27343  cdjreui  27351  cdj3lem2b  27356  addltmulALT  27365  ssrmo  27393  iundifdif  27430  imadifxp  27458  fimacnvinrn2  27476  sspreima  27485  disjdsct  27521  resf1o  27553  xlt2addrd  27578  xrge0infss  27580  ressmulgnn0  27672  xrge0neqmnf  27679  xrge0nre  27680  gsummpt2co  27771  kerunit  27813  locfinreflem  27843  ldlfcntref  27857  pstmfval  27875  mndpluscn  27908  rge0scvg  27931  pnfneige0  27933  pl1cn  27937  nexple  28005  indval2  28028  gsumesum  28067  esumcst  28071  pwsiga  28130  insiga  28137  elsigagen2  28148  measxun2  28181  ddemeas  28208  aean  28216  mbfmfun  28225  mbfmbfm  28229  1stmbfm  28231  2ndmbfm  28232  oms0  28266  sibfof  28282  eulerpartlemt  28310  eulerpartlemmf  28314  eulerpartlemgs2  28319  probun  28358  dstfrvclim1  28416  coinfliprv  28421  ballotlem2  28427  ballotlemfp1  28430  ballotlemic  28445  ballotlem1c  28446  plymulx0  28504  signsvtn0  28527  signstres  28532  cvmliftlem10  28739  mrsub0  28876  mrsubccat  28878  mrsubcn  28879  ghomgrpilem2  29026  risefacp1  29151  fallfacp1  29152  faclim  29171  dfon2lem3  29217  dfon2lem7  29221  dfon2lem8  29222  rdgprc0  29226  wfrlem4  29346  wfrlem5  29347  wfrlem10  29352  wfrlem15  29357  frrlem4  29390  frrlem5  29391  fvsingle  29570  unisnif  29575  funpartlem  29592  hfun  29835  df3nandALT1  29862  lukshef-ax2  29880  nandsym1  29887  finixpnum  30038  fin2so  30040  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  mbfresfi  30061  ftc1cnnc  30089  ftc1anclem6  30095  dvasin  30103  trer  30134  clsun  30146  opnregcld  30148  cldregopn  30149  fnessref  30175  fnopabco  30213  frinfm  30226  nninfnub  30244  caushft  30254  bndss  30282  ispridl2  30435  notornotel1  30495  tsbi2  30541  abeq12  30564  rabeq12f  30565  istopclsd  30632  pellex  30771  monotoddzzfi  30878  jm2.23  30938  expdioph  30965  dford3lem1  30968  wopprc  30972  inisegn0  30989  kelac1  31009  dfac21  31012  lsmfgcl  31020  pwssplit4  31035  isnumbasgrp  31056  dgraalem  31094  lcmcllem  31202  bcc0  31245  pm10.12  31263  pm11.61  31299  sbiota1  31341  fnchoice  31404  elunnel1  31414  elunnel2  31415  suprnmpt  31451  fzisoeu  31500  upbdrech  31505  ssfiunibd  31509  elicore  31537  eliocre  31547  lbioc  31553  fmuldfeq  31577  infrglb  31584  fprodle  31604  mccl  31606  climsuselem1  31613  climsuse  31614  ellimcabssub0  31623  islptre  31625  lptioo2  31637  lptioo1  31638  islpcn  31645  icccncfext  31690  cncfiooicclem1  31696  cncfiooicc  31697  cncfioobdlem  31699  dvbdfbdioo  31727  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  volioc  31771  itgioocnicc  31776  stoweidlem28  31810  stoweidlem52  31834  stoweidlem57  31839  wallispilem3  31849  wallispilem4  31850  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem7  31862  stirlinglem10  31865  stirlinglem12  31867  fourierdlem12  31901  fourierdlem20  31909  fourierdlem25  31914  fourierdlem33  31922  fourierdlem42  31931  fourierdlem48  31937  fourierdlem50  31939  fourierdlem52  31941  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem65  31954  fourierdlem68  31957  fourierdlem70  31959  fourierdlem71  31960  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem80  31969  fourierdlem93  31982  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierswlem  32013  fouriersw  32014  etransclem26  32043  etransclem37  32054  dandysum2p2e4  32170  2reu4a  32194  ndmaovrcl  32289  elpwdifsn  32296  pr1eqbg  32297  el2fzo  32339  usgra2pthlem1  32353  usgra2pth  32354  usgvincvad  32404  usgvincvadALT  32407  usg2edgneu  32412  usgedgvadf1lem2  32414  usgedgvadf1  32415  usgedgvadf1ALTlem2  32417  usgedgvadf1ALT  32418  usgo0s0  32435  usgo0s0ALT  32436  usgo1s0ALT  32437  usgrafisbaseALT  32440  usgrafisbaseALT2  32441  usgo1s0  32442  usgfis  32446  usgfisALT  32450  ressval3d  32558  initoid  32611  termoid  32612  initoeu2lem0  32619  lmod0rng  32674  lidldomnnring  32736  fdmdifeqresdif  32931  altgsumbcALT  32942  ply1sclrmsm  32983  lcoop  33012  lincfsuppcl  33014  linccl  33015  lincvalsng  33017  lincvalpr  33019  lincvalsc0  33022  linc0scn0  33024  lincdifsn  33025  linc1  33026  lincsum  33030  lincscm  33031  lindslinindsimp2lem5  33063  snlindsntor  33072  lincresunit3lem2  33081  ldepsnlinclem1  33106  ldepsnlinclem2  33107  biimp  33250  bi2imp  33251  bi3impb  33252  bi3impa  33253  bi13impib  33255  bi123impib  33256  bi13impia  33257  bi123impia  33258  bi13imp23  33261  bi13imp2  33262  bi12imp3  33263  dfvd1imp  33352  dfvd2imp  33389  e1bi  33415  e2bi  33418  e3bi  33535  3ornot23VD  33647  3impexpbicomVD  33657  3impexpbicomiVD  33658  tratrbVD  33661  ssralv2VD  33666  equncomiVD  33669  truniALTVD  33678  ee33VD  33679  csbingVD  33684  onfrALTlem3VD  33687  onfrALTlem2VD  33689  onfrALTlem1VD  33690  onfrALTVD  33691  csbsngVD  33693  csbxpgVD  33694  csbrngVD  33696  csbunigVD  33698  csbfv12gALTVD  33699  relopabVD  33701  2uasbanhVD  33711  vk15.4jVD  33714  unisnALT  33726  chordthmALT  33733  iunconlem2  33735  bnj529  33798  bnj927  33827  bnj1379  33889  bnj1424  33897  bnj1436  33898  bnj1476  33905  bnj607  33974  bnj908  33989  bnj1097  34037  bnj1118  34040  bnj1128  34046  bnj1145  34049  bnj1154  34055  bnj1174  34059  bnj1189  34065  bnj1204  34068  bnj1388  34089  bnj1417  34097  sylancl2  34168  bj-gl4  34184  bj-babygodel  34191  bj-babylob  34192  bj-alrimhi  34213  bj-nfext  34266  bj-ax9  34464  bj-snsetex  34521  bj-1upln0  34567  bj-inftyexpidisj  34613  bj-elccinfty  34617  lkr0f  34819  glbconN  35101  paddssat  35538  pclunN  35622  2polssN  35639  paddunN  35651  poldmj1N  35652  ltrnnid  35860  dibglbN  36893  bj-ifbi1  37699  rp-fakeanorass  37737  rp-isfinite5  37743  superficl  37752  ssuncl  37755  sssymdifcl  37757  cnvtrrel  37782  trclubg  37785  unhe1  37808  frege55lem1b  37922  frege58bid  37929  imadisjlnd  37973
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 185
  Copyright terms: Public domain W3C validator