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  1011  simp2bi  1012  simp3bi  1013  syl3an1b  1264  syl3an2b  1265  syl3an3b  1266  nic-ax  1490  19.25  1668  sbbii  1718  spvw  1730  hbn1fw  1761  excomim  1799  stdpc5  1855  sb9i  2150  axc11n-16  2261  exmoeu  2311  exmoeuOLD  2312  2mo  2382  2moOLD  2383  2moOLDOLD  2384  eqeq1d  2469  eqeq1OLD  2472  eleq2OLD  2542  gencbvex  3157  moeq  3279  euind  3290  reuind  3307  eqsbc3r  3393  ssel  3498  unssd  3680  ssind  3722  n0moeu  3798  ss0  3816  uneqdifeq  3915  rabsnif  4096  prprc  4139  ssunsn2  4186  eqsn  4188  unisn2  4583  snexALT  4633  reusv3i  4654  snex  4688  brrelex12  5036  elrel  5103  exopxfr2  5145  dmxp  5219  xpssres  5306  elres  5307  elimasni  5362  xpdifid  5433  dmsnsnsn  5484  coi2  5522  xpco  5545  iotabi  5558  uniabio  5559  iotaint  5562  nfunv  5617  funun  5628  funcnv3  5647  funimass1  5659  funssxp  5742  f0dom0  5767  f1o00  5846  dffv3  5860  dffv2  5938  fndmin  5986  iinpreima  6009  fsn2  6059  ftpg  6069  fvn0fvelrn  6076  fnsuppeq0OLD  6120  f12dfv  6165  f13dfv  6166  nvocnv  6173  isoselem  6223  riotaxfrd  6274  oprabid  6306  mpt2difsnif  6377  ovima0  6436  sorpsscmpl  6573  unexg  6583  ordsson  6603  peano2  6698  1stval  6783  2ndval  6784  1stdm  6828  oprabco  6864  f1o2ndf1  6888  poxp  6892  suppval1  6904  funsssuppss  6923  fnsuppeq0  6925  imacosupp  6937  tz7.49c  7108  undifixp  7502  bren2  7543  ensym  7561  en1uniel  7584  domunsn  7664  limenpsi  7689  php4  7701  snnen2o  7703  isinf  7730  en2  7752  findcard2  7756  unfilem1  7780  suppssfifsupp  7840  fsuppunbi  7846  elfiun  7886  marypha1lem  7889  marypha2lem3  7893  supval2  7911  supmaxlem  7920  brwdom2  7995  brwdom3  8004  sucprcreg  8021  preleq  8030  tcmin  8168  prwf  8225  r1pw  8259  rankuni2b  8267  rankr1id  8276  cardval3  8329  ficardom  8338  cardmin2  8375  isinfcard  8469  iscard3  8470  alephval3  8487  dfac9  8512  kmlem6  8531  ackbij1lem12  8607  fin23lem29  8717  fin23lem30  8718  fin23lem41  8728  isf32lem11  8739  isfin1-3  8762  fin1a2lem11  8786  fin1a2lem12  8787  fin1a2lem13  8788  axcc2lem  8812  dominf  8821  axdc4lem  8831  dominfac  8944  pwcfsdom  8954  cfpwsdom  8955  tskuni  9157  wfgru  9190  rpregt0  11229  supxrun  11503  elfz1end  11711  1fv  11785  elfzonlteqm1  11855  fzennn  12042  cardfz  12044  fsuppmapnn0fiubex  12062  fsuppmapnn0fiub0  12063  ser0  12123  crreczi  12255  faclbnd  12332  bcn1  12355  hashrabsn01  12405  hashge0  12419  hashssdif  12436  hashsnlei  12439  euhash1  12441  hashpw  12456  hash2prd  12480  swrd0len0  12619  addlenrevswrd  12620  swrdtrcfv  12627  swrdswrd  12644  swrdccatwrd  12652  swrdccatin2  12671  swrdccat3  12676  swrdccat3a  12678  repsundef  12702  cshwlen  12729  s4f1o  12825  sqrt0  13034  cau3lem  13146  harmonic  13629  mertenslem2  13653  rpnnen2  13816  prmind2  14083  pceq0  14249  prmreclem6  14294  0ram  14393  ram0  14395  cshwsdisj  14437  cshwsiun  14438  ressbas2  14542  ressinbas  14547  mrcuni  14872  mreexexlem4d  14898  catpropd  14961  arwhoma  15226  joinfval  15484  meetfval  15498  clatlem  15594  lubun  15606  psssdm  15699  plusfeq  15742  grpissubg  16016  idrespermg  16231  symgextfv  16238  fvcosymgeq  16249  pmtrprfv3  16275  pmtr3ncomlem1  16294  psgnunilem4  16318  gsummptfzsplitl  16744  gsumzoppg  16758  gsum2dlem1  16788  gsum2dlem2  16789  gsum2d  16790  gsum2dOLD  16791  rngsrg  17024  staffn  17281  scafeq  17315  lbsexg  17593  lidldvgen  17685  ply1bascl2  18014  cply1mul  18106  lply1binom  18119  prmirred  18292  prmirredOLD  18295  zlmassa  18328  frgpcyg  18379  ipfeq  18452  dsmmbas2  18535  frlmbas3  18574  mamufacex  18658  matsubgcell  18703  matinvgcell  18704  matvscacell  18705  mpt2matmul  18715  matepmcl  18731  matepm2cl  18732  mat1dimbas  18741  scmatscm  18782  smatvscl  18793  marrepcl  18833  marepvcl  18838  mulmarep1el  18841  mulmarep1gsum1  18842  mulmarep1gsum2  18843  submabas  18847  nfimdetndef  18858  mdetfval1  18859  m1detdiag  18866  mdetdiag  18868  mdetunilem7  18887  mdetunilem9  18889  m2detleib  18900  gsummatr01lem3  18926  smadiadetlem4  18938  slesolinv  18949  slesolinvbi  18950  slesolex  18951  cramerimplem2  18953  pmatcoe1fsupp  18969  mat2pmatbas  18994  mat2pmatmul  18999  mat2pmatlin  19003  m2cpminvid2lem  19022  decpmatmul  19040  monmatcollpw  19047  pmatcollpw3fi  19053  pm2mpf1  19067  pm2mpghm  19084  fvmptnn04ifb  19119  cayhamlem1  19134  isbasis3g  19217  isopn2  19299  ntrval2  19318  toponmre  19360  innei  19392  restcld  19439  restcldi  19440  neitr  19447  discmp  19664  cmpsublem  19665  cmpsub  19666  2ndcctbss  19722  ptcnp  19858  imasnopn  19926  imasncld  19927  imasncls  19928  kqf  19983  fbun  20076  opnfbas  20078  supfil  20131  ufprim  20145  acufl  20153  filufint  20156  ufldom  20198  hausflf2  20234  alexsubALTlem4  20285  cnextfval  20297  cnextfun  20299  cnextfres  20303  trust  20467  utoptop  20472  ustuqtop1  20479  metustidOLD  20797  metustid  20798  metustfbasOLD  20803  metustfbas  20804  cfilucfilOLD  20807  cfilucfil  20808  metustblOLD  20818  metustbl  20819  restmetu  20825  zlmclm  21330  cphassr  21393  ovolun  21645  volun  21690  vitalilem2  21753  dvmptfsum  22111  rolle  22126  ulmcaulem  22523  logfac  22713  logno1  22745  logreclem  22878  leibpilem1  22999  prmorcht  23180  pclogsum  23218  2sqlem10  23377  chto1lb  23391  tgldimor  23621  ncolne2  23720  axcontlem7  23949  usgraop  24026  ausisusgra  24031  usgra2edg1  24059  usgrarnedg  24060  usgraedg4  24063  usgra1v  24066  usgraidx2vlem2  24068  usgraidx2v  24069  usgrares1  24086  nbgrassvwo  24113  nbgrassvwo2  24114  nb3graprlem2  24128  nb3grapr  24129  nb3grapr2  24130  nb3gra2nb  24131  cusgra3v  24140  cusgrafilem2  24156  usgrasscusgra  24159  uvtxnbgra  24169  uvtxnb  24173  2trllemH  24230  2trllemE  24231  constr1trl  24266  usgra2adedgwlkonALT  24292  usgra2wlkspthlem2  24296  fargshiftfo  24314  wwlknndef  24413  wwlkextproplem3  24419  clwlkswlks  24434  clwwlknndef  24449  clwlkisclwwlklem2a4  24460  clwlkisclwwlklem1  24463  clwwlkf  24470  clwwlkvbij  24477  wwlkext2clwwlk  24479  clwwnisshclwwn  24485  erclwwlkref  24489  erclwwlknref  24501  erclwwlknsym  24502  erclwwlkntr  24503  hashecclwwlkn1  24510  usghashecclwwlk  24511  clwlkfoclwwlk  24521  el2wlkonot  24545  el2spthonot  24546  el2wlkonotot0  24548  vdgrnn0pnf  24585  clwlknclwlkdifs  24636  eupatrl  24644  frgra3v  24678  3vfriswmgra  24681  1to3vfriswmgra  24683  1to3vfriendship  24684  2pthfrgra  24687  4cycl2v2nb  24692  n4cyclfrgra  24694  frgranbnb  24696  frgrancvvdeqlem4  24710  frgrawopreg  24726  frg2woteqm  24736  usg2spot2nb  24742  numclwwlkovf2ex  24763  numclwwlk3lem  24785  grpoidinvlem3  24884  nmlno0lem  25384  blocni  25396  pythi  25441  normpythi  25735  shmodsi  25983  omlsilem  25996  pjchi  26026  chlubii  26066  osumi  26236  nmlnop0iALT  26590  cnlnssadj  26675  nmopcoi  26690  mdbr3  26892  mdbr4  26893  ssmd1  26906  dmdsl3  26910  mdslmd1lem2  26921  mdslmd4i  26928  mdexchi  26930  atssma  26973  atoml2i  26978  chirredlem3  26987  mdsymlem1  26998  mdsymlem3  27000  dmdbr6ati  27018  dmdbr7ati  27019  cdjreui  27027  cdj3lem2b  27032  addltmulALT  27041  ssrmo  27069  iundifdif  27103  imadifxp  27131  fcoinver  27133  fimacnvinrn2  27149  sspreima  27157  disjdsct  27193  resf1o  27225  fpwrelmap  27228  xlt2addrd  27246  xrge0infss  27248  ressmulgnn0  27334  xrge0neqmnf  27341  xrge0nre  27342  gsummpt2co  27434  kerunit  27476  pstmfval  27511  mndpluscn  27544  rge0scvg  27567  pnfneige0  27569  pl1cn  27573  nexple  27645  indval2  27668  gsumesum  27707  esumcst  27711  pwsiga  27770  insiga  27777  elsigagen2  27788  measxun2  27821  ddemeas  27848  aean  27856  mbfmfun  27865  mbfmbfm  27869  1stmbfm  27871  2ndmbfm  27872  oms0  27906  sibfof  27922  eulerpartlemt  27950  eulerpartlemmf  27954  eulerpartlemgs2  27959  probun  27998  dstfrvclim1  28056  coinfliprv  28061  ballotlem2  28067  ballotlemfp1  28070  ballotlemic  28085  ballotlem1c  28086  plymulx0  28144  signsvtn0  28167  signstres  28172  cvmliftlem10  28379  ghomgrpilem2  28501  prodf1  28602  fprodfac  28679  risefacp1  28728  fallfacp1  28729  faclim  28748  dfon2lem3  28794  dfon2lem7  28798  dfon2lem8  28799  rdgprc0  28803  wfrlem4  28923  wfrlem5  28924  wfrlem10  28929  wfrlem15  28934  frrlem4  28967  frrlem5  28968  fvsingle  29147  unisnif  29152  funpartlem  29169  hfun  29412  df3nandALT1  29439  lukshef-ax2  29457  nandsym1  29464  finixpnum  29615  fin2so  29617  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  mbfresfi  29638  ftc1cnnc  29666  ftc1anclem6  29672  dvasin  29680  trer  29711  clsun  29723  opnregcld  29725  cldregopn  29726  ssref  29755  fnessref  29765  fnopabco  29816  frinfm  29829  nninfnub  29847  caushft  29857  bndss  29885  ispridl2  30038  notornotel1  30098  tsbi2  30145  abeq12  30168  rabeq12f  30169  istopclsd  30236  pellex  30375  rmspecsqrtnq  30446  monotoddzzfi  30482  jm2.23  30542  expdioph  30569  dford3lem1  30572  wopprc  30576  inisegn0  30593  kelac1  30613  dfac21  30616  lsmfgcl  30624  pwssplit4  30639  isnumbasgrp  30660  dgraalem  30699  lcmcllem  30802  pm10.12  30841  pm11.61  30877  sbiota1  30919  fnchoice  30982  elunnel1  30992  elunnel2  30993  elinel2  31002  elinel1  31003  suprnmpt  31029  fzisoeu  31077  upbdrech  31082  ssfiunibd  31086  elicore  31101  eliocre  31111  lbioc  31117  fmuldfeq  31133  infrglb  31140  climsuselem1  31149  climsuse  31150  ellimcabssub0  31159  islptre  31161  lptioo2  31173  lptioo1  31174  islpcn  31181  icccncfext  31226  cncfiooicclem1  31232  cncfiooicc  31233  cncfioobdlem  31235  dvbdfbdioo  31260  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  volioc  31290  itgioocnicc  31295  iblcncfioo  31296  stoweidlem28  31328  stoweidlem52  31352  stoweidlem57  31357  wallispilem3  31367  wallispilem4  31368  wallispi  31370  wallispi2lem1  31371  wallispi2lem2  31372  wallispi2  31373  stirlinglem7  31380  stirlinglem10  31383  stirlinglem12  31385  fourierdlem12  31419  fourierdlem20  31427  fourierdlem25  31432  fourierdlem33  31440  fourierdlem42  31449  fourierdlem48  31455  fourierdlem50  31457  fourierdlem52  31459  fourierdlem57  31464  fourierdlem58  31465  fourierdlem59  31466  fourierdlem62  31469  fourierdlem65  31472  fourierdlem68  31475  fourierdlem70  31477  fourierdlem71  31478  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem80  31487  fourierdlem87  31494  fourierdlem93  31500  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourier2  31528  fourierswlem  31531  fouriersw  31532  dandysum2p2e4  31637  2reu4a  31661  ndmaovrcl  31756  elpwdifsn  31763  pr1eqbg  31764  el2fzo  31808  usgra2pthlem1  31822  usgra2pth  31823  usgvincvad  31873  usgvincvadALT  31876  usg2edgneu  31881  usgedgvadf1lem2  31883  usgedgvadf1  31884  usgedgvadf1ALTlem2  31886  usgedgvadf1ALT  31887  usgo0s0  31904  usgo0s0ALT  31905  usgo1s0ALT  31906  usgrafisbaseALT  31909  usgrafisbaseALT2  31910  usgo1s0  31911  usgfis  31915  usgfisALT  31919  fdmdifeqresdif  31995  altgsumbcALT  32006  lmod0rng  32032  ply1sclrmsm  32056  lcoop  32085  lincfsuppcl  32087  linccl  32088  lincvalsng  32090  lincvalpr  32092  lincvalsc0  32095  linc0scn0  32097  lincdifsn  32098  linc1  32099  lincsum  32103  lincscm  32104  lindslinindsimp2lem5  32136  snlindsntor  32145  lincresunit3lem2  32154  ldepsnlinclem1  32187  ldepsnlinclem2  32188  biimp  32329  bi2imp  32330  bi3impb  32331  bi3impa  32332  bi13impib  32334  bi123impib  32335  bi13impia  32336  bi123impia  32337  bi13imp23  32340  bi13imp2  32341  bi12imp3  32342  dfvd1imp  32432  dfvd2imp  32469  e1bi  32495  e2bi  32498  e3bi  32615  3ornot23VD  32727  3impexpbicomVD  32737  3impexpbicomiVD  32738  tratrbVD  32741  ssralv2VD  32746  equncomiVD  32749  truniALTVD  32758  ee33VD  32759  csbingVD  32764  onfrALTlem3VD  32767  onfrALTlem2VD  32769  onfrALTlem1VD  32770  onfrALTVD  32771  csbsngVD  32773  csbxpgVD  32774  csbrngVD  32776  csbunigVD  32778  csbfv12gALTVD  32779  relopabVD  32781  2uasbanhVD  32791  vk15.4jVD  32794  unisnALT  32806  chordthmALT  32813  iunconlem2  32815  bnj529  32877  bnj927  32906  bnj1379  32968  bnj1424  32976  bnj1436  32977  bnj1476  32984  bnj607  33053  bnj908  33068  bnj1097  33116  bnj1118  33119  bnj1128  33125  bnj1145  33128  bnj1154  33134  bnj1174  33138  bnj1189  33144  bnj1204  33147  bnj1388  33168  bnj1417  33176  sylancl2  33249  bj-gl4  33266  bj-babygodel  33273  bj-babylob  33274  bj-alrimhi  33301  bj-nfext  33348  bj-ax9  33545  bj-snsetex  33602  bj-1upln0  33648  bj-inftyexpidisj  33685  bj-elccinfty  33689  lkr0f  33891  glbconN  34173  paddssat  34610  pclunN  34694  2polssN  34711  paddunN  34723  poldmj1N  34724  ltrnnid  34932  dibglbN  35963  superficl  36772  ssuncl  36775  sssymdifcl  36777  cnvtrrel  36792  trclubg  36795  bj-frege52a  36868  bj-frege54cor1a  36873  frege55aid  36874  frege55lem1b  36887  frege54cor1c  36907  frege58newc  36913
  Copyright terms: Public domain W3C validator