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

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

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2  |-  ( ph  <->  ps )
2 bi1 186 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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
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  846  pm5.15  887  pm5.16  888  pm5.75  935  rnlemOLD  963  simp1bi  1010  simp2bi  1011  simp3bi  1012  syl3an1b  1263  syl3an2b  1264  syl3an3b  1265  nic-ax  1491  19.25  1676  stdpc5v  1717  sbbii  1731  spvw  1741  excomim  1834  stdpc5  1892  sb9i  2154  axc11n-16  2252  exmoeu  2300  2mo  2357  2moOLD  2358  eqeq1d  2443  eqeq1OLD  2446  eleq2OLD  2516  gencbvex  3137  moeq  3259  euind  3270  reuind  3287  eqsbc3r  3373  ra4v  3407  ra4  3409  ssel  3481  unssd  3663  ssind  3705  n0moeu  3781  ss0  3799  uneqdifeq  3899  rabsnif  4081  prprc  4124  ssunsn2  4171  eqsn  4173  unisn2  4570  snexALT  4620  reusv3i  4641  snex  4675  brrelex12  5024  elrel  5092  exopxfr2  5134  dmxp  5208  xpssres  5295  elres  5296  elimasni  5351  xpdifid  5422  dmsnsnsn  5473  coi2  5511  xpco  5534  iotabi  5547  uniabio  5548  iotaint  5551  nfunv  5606  funun  5617  funcnv3  5636  funimass1  5648  funssxp  5731  f0dom0  5756  f1o00  5835  dffv3  5849  dffv2  5928  fndmin  5976  iinpreima  5999  fveqressseq  6009  fsn2  6053  ftpg  6063  fnsuppeq0OLD  6114  f12dfv  6161  f13dfv  6162  nvocnv  6169  isoselem  6219  riotaxfrd  6270  oprabid  6305  mpt2difsnif  6377  ovima0  6436  sorpsscmpl  6573  unexg  6583  ordsson  6607  peano2  6702  1stval  6784  2ndval  6785  1stdm  6829  oprabco  6866  f1o2ndf1  6890  poxp  6894  suppval1  6906  funsssuppss  6925  fnsuppeq0  6927  imacosupp  6939  tz7.49c  7110  undifixp  7504  bren2  7545  ensym  7563  en1uniel  7586  domunsn  7666  limenpsi  7691  php4  7703  snnen2o  7705  isinf  7732  en2  7755  findcard2  7759  unfilem1  7783  suppssfifsupp  7843  fsuppunbi  7849  elfiun  7889  marypha1lem  7892  marypha2lem3  7896  supval2  7914  supmaxlemOLD  7924  brwdom2  7999  brwdom3  8008  sucprcreg  8025  preleq  8034  tcmin  8172  prwf  8229  r1pw  8263  rankuni2b  8271  rankr1id  8280  cardval3  8333  ficardom  8342  cardmin2  8379  isinfcard  8473  iscard3  8474  alephval3  8491  dfac9  8516  kmlem6  8535  ackbij1lem12  8611  fin23lem29  8721  fin23lem30  8722  fin23lem41  8732  isf32lem11  8743  isfin1-3  8766  fin1a2lem11  8790  fin1a2lem12  8791  fin1a2lem13  8792  axcc2lem  8816  dominf  8825  axdc4lem  8835  dominfac  8948  pwcfsdom  8958  cfpwsdom  8959  tskuni  9161  wfgru  9194  rpregt0  11239  supxrun  11513  elfz1end  11721  1fv  11797  elfzonlteqm1  11867  fzennn  12054  cardfz  12056  fsuppmapnn0fiubex  12074  fsuppmapnn0fiub0  12075  ser0  12135  crreczi  12267  faclbnd  12344  bcn1  12367  hashrabsn01  12417  hashge0  12431  hashssdif  12451  hashsnlei  12454  hashpw  12470  hash2prd  12494  swrd0len0  12636  swrdtrcfv  12644  swrdswrd  12661  swrdccatwrd  12669  swrdccatin2  12688  swrdccat3  12693  swrdccat3a  12695  repsundef  12719  cshwlen  12746  s4f1o  12842  sqrt0  13051  cau3lem  13163  harmonic  13646  mertenslem2  13670  rpnnen2  13833  prmind2  14102  pceq0  14268  prmreclem6  14313  0ram  14412  ram0  14414  cshwsdisj  14457  cshwsiun  14458  ressbas2  14562  ressinbas  14567  mrcuni  14892  mreexexlem4d  14918  catpropd  14978  arwhoma  15243  joinfval  15502  meetfval  15516  clatlem  15612  lubun  15624  psssdm  15717  ismgmn0  15745  plusfeq  15750  isnsgrp  15786  isnmnd  15795  grpissubg  16092  idrespermg  16307  symgextfv  16314  fvcosymgeq  16325  pmtrprfv3  16350  pmtr3ncomlem1  16369  psgnunilem4  16393  gsummptfzsplitl  16824  gsumzoppg  16838  gsum2dlem1  16868  gsum2dlem2  16869  gsum2d  16870  gsum2dOLD  16871  srg1zr  17051  staffn  17369  scafeq  17403  lbsexg  17681  lidldvgen  17774  ply1bascl2  18114  cply1mul  18206  lply1binom  18219  prmirred  18395  prmirredOLD  18398  zlmassa  18431  frgpcyg  18482  ipfeq  18555  dsmmbas2  18638  frlmbas3  18677  mamufacex  18761  matsubgcell  18806  matinvgcell  18807  matvscacell  18808  mpt2matmul  18818  matepmcl  18834  matepm2cl  18835  mat1dimbas  18844  scmatscm  18885  smatvscl  18896  marrepcl  18936  marepvcl  18941  mulmarep1el  18944  mulmarep1gsum1  18945  mulmarep1gsum2  18946  submabas  18950  nfimdetndef  18961  mdetfval1  18962  m1detdiag  18969  mdetdiag  18971  mdetunilem7  18990  mdetunilem9  18992  m2detleib  19003  gsummatr01lem3  19029  smadiadetlem4  19041  slesolinv  19052  slesolinvbi  19053  slesolex  19054  cramerimplem2  19056  pmatcoe1fsupp  19072  mat2pmatbas  19097  mat2pmatmul  19102  mat2pmatlin  19106  m2cpminvid2lem  19125  decpmatmul  19143  monmatcollpw  19150  pmatcollpw3fi  19156  pm2mpf1  19170  pm2mpghm  19187  fvmptnn04ifb  19222  cayhamlem1  19237  isbasis3g  19320  isopn2  19403  ntrval2  19422  toponmre  19464  innei  19496  restcld  19543  restcldi  19544  neitr  19551  discmp  19768  cmpsublem  19769  cmpsub  19770  2ndcctbss  19826  ssref  19883  lfinun  19896  dissnref  19899  ptcnp  19993  imasnopn  20061  imasncld  20062  imasncls  20063  kqf  20118  fbun  20211  opnfbas  20213  supfil  20266  ufprim  20280  acufl  20288  filufint  20291  ufldom  20333  hausflf2  20369  alexsubALTlem4  20420  cnextfval  20432  cnextfun  20434  cnextfres  20438  trust  20602  utoptop  20607  ustuqtop1  20614  metustidOLD  20932  metustid  20933  metustfbasOLD  20938  metustfbas  20939  cfilucfilOLD  20942  cfilucfil  20943  metustblOLD  20953  metustbl  20954  restmetu  20960  zlmclm  21465  cphassr  21528  ovolun  21780  volun  21825  vitalilem2  21888  dvmptfsum  22246  rolle  22261  ulmcaulem  22658  logfac  22854  logno1  22886  logreclem  23019  leibpilem1  23140  prmorcht  23321  pclogsum  23359  2sqlem10  23518  chto1lb  23532  tgldimor  23762  axcontlem7  24142  usgraop  24219  ausisusgra  24224  usgra2edg1  24252  usgrarnedg  24253  usgraedg4  24256  usgra1v  24259  usgraidx2vlem2  24261  usgraidx2v  24262  usgrares1  24279  nbgrassvwo  24306  nbgrassvwo2  24307  nb3graprlem2  24321  nb3grapr  24322  nb3grapr2  24323  nb3gra2nb  24324  cusgra3v  24333  cusgrafilem2  24349  usgrasscusgra  24352  uvtxnbgra  24362  uvtxnb  24366  2trllemH  24423  2trllemE  24424  constr1trl  24459  usgra2adedgwlkonALT  24485  usgra2wlkspthlem2  24489  fargshiftfo  24507  wwlknndef  24606  wwlkextproplem3  24612  clwlkswlks  24627  clwwlknndef  24642  clwlkisclwwlklem2a4  24653  clwlkisclwwlklem1  24656  clwwlkf  24663  clwwlkvbij  24670  wwlkext2clwwlk  24672  clwwnisshclwwn  24678  erclwwlkref  24682  erclwwlknref  24694  erclwwlknsym  24695  erclwwlkntr  24696  hashecclwwlkn1  24703  usghashecclwwlk  24704  clwlkfoclwwlk  24714  el2wlkonot  24738  el2spthonot  24739  el2wlkonotot0  24741  vdgrnn0pnf  24778  clwlknclwlkdifs  24829  eupatrl  24837  frgra3v  24871  3vfriswmgra  24874  1to3vfriswmgra  24876  1to3vfriendship  24877  2pthfrgra  24880  4cycl2v2nb  24885  n4cyclfrgra  24887  frgranbnb  24889  frgrancvvdeqlem4  24902  frgrawopreg  24918  frg2woteqm  24928  usg2spot2nb  24934  numclwwlkovf2ex  24955  numclwwlk3lem  24977  grpoidinvlem3  25077  nmlno0lem  25577  blocni  25589  pythi  25634  normpythi  25928  shmodsi  26176  omlsilem  26189  pjchi  26219  chlubii  26259  osumi  26429  nmlnop0iALT  26783  cnlnssadj  26868  nmopcoi  26883  mdbr3  27085  mdbr4  27086  ssmd1  27099  dmdsl3  27103  mdslmd1lem2  27114  mdslmd4i  27121  mdexchi  27123  atssma  27166  atoml2i  27171  chirredlem3  27180  mdsymlem1  27191  mdsymlem3  27193  dmdbr6ati  27211  dmdbr7ati  27212  cdjreui  27220  cdj3lem2b  27225  addltmulALT  27234  ssrmo  27262  iundifdif  27299  imadifxp  27327  fimacnvinrn2  27345  sspreima  27354  disjdsct  27390  resf1o  27422  xlt2addrd  27447  xrge0infss  27449  ressmulgnn0  27542  xrge0neqmnf  27549  xrge0nre  27550  gsummpt2co  27641  kerunit  27683  locfinreflem  27713  ldlfcntref  27727  pstmfval  27745  mndpluscn  27778  rge0scvg  27801  pnfneige0  27803  pl1cn  27807  nexple  27875  indval2  27898  gsumesum  27937  esumcst  27941  pwsiga  28000  insiga  28007  elsigagen2  28018  measxun2  28051  ddemeas  28078  aean  28086  mbfmfun  28095  mbfmbfm  28099  1stmbfm  28101  2ndmbfm  28102  oms0  28136  sibfof  28152  eulerpartlemt  28180  eulerpartlemmf  28184  eulerpartlemgs2  28189  probun  28228  dstfrvclim1  28286  coinfliprv  28291  ballotlem2  28297  ballotlemfp1  28300  ballotlemic  28315  ballotlem1c  28316  plymulx0  28374  signsvtn0  28397  signstres  28402  cvmliftlem10  28609  mrsub0  28746  mrsubccat  28748  mrsubcn  28749  ghomgrpilem2  28896  prodf1  28997  fprodfac  29074  risefacp1  29123  fallfacp1  29124  faclim  29143  dfon2lem3  29189  dfon2lem7  29193  dfon2lem8  29194  rdgprc0  29198  wfrlem4  29318  wfrlem5  29319  wfrlem10  29324  wfrlem15  29329  frrlem4  29362  frrlem5  29363  fvsingle  29542  unisnif  29547  funpartlem  29564  hfun  29807  df3nandALT1  29834  lukshef-ax2  29852  nandsym1  29859  finixpnum  30010  fin2so  30012  mblfinlem2  30024  mblfinlem3  30025  mblfinlem4  30026  ismblfin  30027  mbfresfi  30033  ftc1cnnc  30061  ftc1anclem6  30067  dvasin  30075  trer  30106  clsun  30118  opnregcld  30120  cldregopn  30121  fnessref  30147  fnopabco  30185  frinfm  30198  nninfnub  30216  caushft  30226  bndss  30254  ispridl2  30407  notornotel1  30467  tsbi2  30513  abeq12  30536  rabeq12f  30537  istopclsd  30604  pellex  30743  monotoddzzfi  30850  jm2.23  30910  expdioph  30937  dford3lem1  30940  wopprc  30944  inisegn0  30961  kelac1  30981  dfac21  30984  lsmfgcl  30992  pwssplit4  31007  isnumbasgrp  31028  dgraalem  31067  lcmcllem  31175  pm10.12  31214  pm11.61  31250  sbiota1  31292  fnchoice  31355  elunnel1  31365  elunnel2  31366  suprnmpt  31401  fzisoeu  31449  upbdrech  31454  ssfiunibd  31458  elicore  31473  eliocre  31483  lbioc  31489  fmuldfeq  31505  infrglb  31512  climsuselem1  31521  climsuse  31522  ellimcabssub0  31531  islptre  31533  lptioo2  31545  lptioo1  31546  islpcn  31553  icccncfext  31597  cncfiooicclem1  31603  cncfiooicc  31604  cncfioobdlem  31606  dvbdfbdioo  31631  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  volioc  31661  itgioocnicc  31666  stoweidlem28  31699  stoweidlem52  31723  stoweidlem57  31728  wallispilem3  31738  wallispilem4  31739  wallispi  31741  wallispi2lem1  31742  wallispi2lem2  31743  wallispi2  31744  stirlinglem7  31751  stirlinglem10  31754  stirlinglem12  31756  fourierdlem12  31790  fourierdlem20  31798  fourierdlem25  31803  fourierdlem33  31811  fourierdlem42  31820  fourierdlem48  31826  fourierdlem50  31828  fourierdlem52  31830  fourierdlem57  31835  fourierdlem58  31836  fourierdlem59  31837  fourierdlem65  31843  fourierdlem68  31846  fourierdlem70  31848  fourierdlem71  31849  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem80  31858  fourierdlem93  31871  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierswlem  31902  fouriersw  31903  dandysum2p2e4  32008  2reu4a  32032  ndmaovrcl  32127  elpwdifsn  32134  pr1eqbg  32135  el2fzo  32177  usgra2pthlem1  32191  usgra2pth  32192  usgvincvad  32242  usgvincvadALT  32245  usg2edgneu  32250  usgedgvadf1lem2  32252  usgedgvadf1  32253  usgedgvadf1ALTlem2  32255  usgedgvadf1ALT  32256  usgo0s0  32273  usgo0s0ALT  32274  usgo1s0ALT  32275  usgrafisbaseALT  32278  usgrafisbaseALT2  32279  usgo1s0  32280  usgfis  32284  usgfisALT  32288  ressval3d  32393  lidldomnnring  32443  fdmdifeqresdif  32659  altgsumbcALT  32670  lmod0rng  32689  ply1sclrmsm  32713  lcoop  32742  lincfsuppcl  32744  linccl  32745  lincvalsng  32747  lincvalpr  32749  lincvalsc0  32752  linc0scn0  32754  lincdifsn  32755  linc1  32756  lincsum  32760  lincscm  32761  lindslinindsimp2lem5  32793  snlindsntor  32802  lincresunit3lem2  32811  ldepsnlinclem1  32836  ldepsnlinclem2  32837  biimp  32978  bi2imp  32979  bi3impb  32980  bi3impa  32981  bi13impib  32983  bi123impib  32984  bi13impia  32985  bi123impia  32986  bi13imp23  32989  bi13imp2  32990  bi12imp3  32991  dfvd1imp  33080  dfvd2imp  33117  e1bi  33143  e2bi  33146  e3bi  33263  3ornot23VD  33375  3impexpbicomVD  33385  3impexpbicomiVD  33386  tratrbVD  33389  ssralv2VD  33394  equncomiVD  33397  truniALTVD  33406  ee33VD  33407  csbingVD  33412  onfrALTlem3VD  33415  onfrALTlem2VD  33417  onfrALTlem1VD  33418  onfrALTVD  33419  csbsngVD  33421  csbxpgVD  33422  csbrngVD  33424  csbunigVD  33426  csbfv12gALTVD  33427  relopabVD  33429  2uasbanhVD  33439  vk15.4jVD  33442  unisnALT  33454  chordthmALT  33461  iunconlem2  33463  bnj529  33526  bnj927  33555  bnj1379  33617  bnj1424  33625  bnj1436  33626  bnj1476  33633  bnj607  33702  bnj908  33717  bnj1097  33765  bnj1118  33768  bnj1128  33774  bnj1145  33777  bnj1154  33783  bnj1174  33787  bnj1189  33793  bnj1204  33796  bnj1388  33817  bnj1417  33825  sylancl2  33903  bj-gl4  33919  bj-babygodel  33926  bj-babylob  33927  bj-alrimhi  33948  bj-nfext  34001  bj-ax9  34197  bj-snsetex  34254  bj-1upln0  34300  bj-inftyexpidisj  34336  bj-elccinfty  34340  lkr0f  34542  glbconN  34824  paddssat  35261  pclunN  35345  2polssN  35362  paddunN  35374  poldmj1N  35375  ltrnnid  35583  dibglbN  36616  rp-fakeanorass  37423  rp-isfinite5  37429  superficl  37438  ssuncl  37441  sssymdifcl  37443  cnvtrrel  37458  trclubg  37461  unhe1  37478  frege55lem1b  37573  frege58bid  37579  imadisjlnd  37625
  Copyright terms: Public domain W3C validator