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  844  pm5.15  884  pm5.16  885  pm5.75  928  rnlem  956  simp1bi  1003  simp2bi  1004  simp3bi  1005  syl3an1b  1255  syl3an2b  1256  syl3an3b  1257  nic-ax  1481  19.25  1659  sbbii  1709  spvw  1721  hbn1fw  1752  excomim  1790  stdpc5  1843  sb9i  2134  axc11n-16  2246  exmoeu  2296  exmoeuOLD  2297  2mo  2367  2moOLD  2368  2moOLDOLD  2369  eqeq1d  2453  eqeq1OLD  2456  eleq2OLD  2526  gencbvex  3112  moeq  3232  euind  3243  reuind  3260  eqsbc3r  3346  ssel  3448  unssd  3630  ssind  3672  n0moeu  3748  ss0  3766  uneqdifeq  3865  rabsnif  4042  prprc  4085  ssunsn2  4130  eqsn  4132  unisn2  4526  snexALT  4576  reusv3i  4597  snex  4631  brrelex12  4974  elrel  5040  exopxfr2  5082  dmxp  5156  xpssres  5242  elres  5243  elimasni  5294  xpdifid  5364  dmsnsnsn  5415  coi2  5452  xpco  5475  iotabi  5488  uniabio  5489  iotaint  5492  nfunv  5547  funun  5558  funcnv3  5577  funimass1  5589  funssxp  5669  f0dom0  5693  f1o00  5771  dffv3  5785  dffv2  5863  fndmin  5909  iinpreima  5932  fsn2  5982  ftpg  5991  fnsuppeq0OLD  6038  nvocnv  6087  isoselem  6131  riotaxfrd  6182  oprabid  6214  mpt2difsnif  6283  ovima0  6342  sorpsscmpl  6471  unexg  6481  ordsson  6501  peano2  6596  1stval  6679  2ndval  6680  1stdm  6721  oprabco  6757  f1o2ndf1  6780  poxp  6784  suppval1  6796  funsssuppss  6815  fnsuppeq0  6817  imacosupp  6829  tz7.49c  7001  undifixp  7399  bren2  7440  ensym  7458  en1uniel  7481  domunsn  7561  limenpsi  7586  php4  7598  snnen2o  7600  isinf  7627  en2  7649  findcard2  7653  unfilem1  7677  suppssfifsupp  7736  fsuppunbi  7742  elfiun  7781  marypha1lem  7784  marypha2lem3  7788  supval2  7806  supmaxlem  7815  brwdom2  7889  brwdom3  7898  sucprcreg  7915  preleq  7924  tcmin  8062  prwf  8119  r1pw  8153  rankuni2b  8161  rankr1id  8170  cardval3  8223  ficardom  8232  cardmin2  8269  isinfcard  8363  iscard3  8364  alephval3  8381  dfac9  8406  kmlem6  8425  ackbij1lem12  8501  fin23lem29  8611  fin23lem30  8612  fin23lem41  8622  isf32lem11  8633  isfin1-3  8656  fin1a2lem11  8680  fin1a2lem12  8681  fin1a2lem13  8682  axcc2lem  8706  dominf  8715  axdc4lem  8725  dominfac  8838  pwcfsdom  8848  cfpwsdom  8849  tskuni  9051  wfgru  9084  rpregt0  11105  supxrun  11379  elfz1end  11580  1fv  11633  fzennn  11891  cardfz  11893  ser0  11959  crreczi  12090  faclbnd  12167  bcn1  12190  hashge0  12252  hashssdif  12269  hashsnlei  12272  euhash1  12274  hash2prd  12283  hashpw  12300  swrd0len0  12431  addlenrevswrd  12432  swrdtrcfv  12439  swrdswrd  12456  swrdccatwrd  12464  swrdccatin2  12480  swrdccat3  12485  swrdccat3a  12487  repsundef  12511  cshwlen  12538  s4f1o  12630  sqr0  12833  cau3lem  12944  harmonic  13423  mertenslem2  13447  rpnnen2  13610  prmind2  13876  pceq0  14039  prmreclem6  14084  0ram  14183  ram0  14185  cshwsdisj  14227  cshwsiun  14228  ressbas2  14331  ressinbas  14336  mrcuni  14661  mreexexlem4d  14687  catpropd  14750  arwhoma  15015  joinfval  15273  meetfval  15287  clatlem  15383  lubun  15395  psssdm  15488  plusfeq  15531  grpissubg  15803  idrespermg  16018  symgextfv  16025  fvcosymgeq  16036  pmtrprfv3  16062  pmtr3ncomlem1  16081  psgnunilem4  16105  gsummptfzsplitl  16531  gsumzoppg  16545  gsum2dlem1  16566  gsum2dlem2  16567  gsum2d  16568  gsum2dOLD  16569  rngsrg  16789  staffn  17040  scafeq  17074  lbsexg  17351  lidldvgen  17443  ply1bascl2  17767  prmirred  18028  prmirredOLD  18031  zlmassa  18064  frgpcyg  18115  ipfeq  18188  dsmmbas2  18271  frlmbas3  18310  mamufacex  18398  matepmcl  18458  matepm2cl  18459  marrepcl  18486  marepvcl  18491  mulmarep1el  18494  mulmarep1gsum1  18495  mulmarep1gsum2  18496  submabas  18500  nfimdetndef  18511  mdetfval1  18512  m1detdiag  18519  mdetdiag  18521  mdetunilem7  18540  mdetunilem9  18542  m2detleib  18553  gsummatr01lem3  18579  smadiadetlem4  18591  slesolinv  18602  slesolinvbi  18603  slesolex  18604  cramerimplem2  18606  isbasis3g  18670  isopn2  18752  ntrval2  18771  toponmre  18813  innei  18845  restcld  18892  restcldi  18893  neitr  18900  discmp  19117  cmpsublem  19118  cmpsub  19119  2ndcctbss  19175  ptcnp  19311  imasnopn  19379  imasncld  19380  imasncls  19381  kqf  19436  fbun  19529  opnfbas  19531  supfil  19584  ufprim  19598  acufl  19606  filufint  19609  ufldom  19651  hausflf2  19687  alexsubALTlem4  19738  cnextfval  19750  cnextfun  19752  cnextfres  19756  trust  19920  utoptop  19925  ustuqtop1  19932  metustidOLD  20250  metustid  20251  metustfbasOLD  20256  metustfbas  20257  cfilucfilOLD  20260  cfilucfil  20261  metustblOLD  20271  metustbl  20272  restmetu  20278  zlmclm  20783  cphassr  20846  ovolun  21098  volun  21142  vitalilem2  21205  dvmptfsum  21563  rolle  21578  ulmcaulem  21975  logfac  22165  logno1  22197  logreclem  22330  leibpilem1  22451  prmorcht  22632  pclogsum  22670  2sqlem10  22829  chto1lb  22843  tgldimor  23073  ncolne2  23154  axcontlem7  23351  ausisusgra  23414  usgra2edg1  23437  usgrarnedg  23438  usgraedg4  23440  usgra1v  23443  usgraidx2vlem2  23445  usgraidx2v  23446  usgrares1  23458  nb3graprlem2  23495  nb3grapr  23496  nb3grapr2  23497  nb3gra2nb  23498  cusgra3v  23507  cusgrafilem2  23523  usgrasscusgra  23526  uvtxnbgra  23536  2trllemH  23586  2trllemE  23587  constr1trl  23622  fargshiftfo  23659  vdgrnn0pnf  23714  eupatrl  23724  grpoidinvlem3  23828  nmlno0lem  24328  blocni  24340  pythi  24385  normpythi  24679  shmodsi  24927  omlsilem  24940  pjchi  24970  chlubii  25010  osumi  25180  nmlnop0iALT  25534  cnlnssadj  25619  nmopcoi  25634  mdbr3  25836  mdbr4  25837  ssmd1  25850  dmdsl3  25854  mdslmd1lem2  25865  mdslmd4i  25872  mdexchi  25874  atssma  25917  atoml2i  25922  chirredlem3  25931  mdsymlem1  25942  mdsymlem3  25944  dmdbr6ati  25962  dmdbr7ati  25963  cdjreui  25971  cdj3lem2b  25976  addltmulALT  25985  ssrmo  26013  iundifdif  26047  imadifxp  26073  fimacnvinrn2  26087  sspreima  26096  disjdsct  26132  resf1o  26164  fpwrelmap  26167  xlt2addrd  26185  xrge0infss  26187  ressmulgnn0  26279  xrge0neqmnf  26286  xrge0nre  26287  gsummpt2co  26383  kerunit  26425  pstmfval  26457  mndpluscn  26490  rge0scvg  26513  pnfneige0  26515  pl1cn  26519  nexple  26582  indval2  26605  gsumesum  26644  esumcst  26648  pwsiga  26707  insiga  26714  elsigagen2  26725  measxun2  26758  ddemeas  26786  aean  26794  mbfmfun  26803  mbfmbfm  26807  1stmbfm  26809  2ndmbfm  26810  oms0  26844  sibfof  26860  eulerpartlemt  26888  eulerpartlemmf  26892  eulerpartlemgs2  26897  probun  26936  dstfrvclim1  26994  coinfliprv  26999  ballotlem2  27005  ballotlemfp1  27008  ballotlemic  27023  ballotlem1c  27024  plymulx0  27082  signsvtn0  27105  signstres  27110  cvmliftlem10  27317  ghomgrpilem2  27439  prodf1  27540  fprodfac  27617  risefacp1  27666  fallfacp1  27667  faclim  27686  dfon2lem3  27732  dfon2lem7  27736  dfon2lem8  27737  rdgprc0  27741  wfrlem4  27861  wfrlem5  27862  wfrlem10  27867  wfrlem15  27872  frrlem4  27905  frrlem5  27906  fvsingle  28085  unisnif  28090  funpartlem  28107  hfun  28350  df3nandALT1  28377  lukshef-ax2  28395  nandsym1  28402  finixpnum  28552  fin2so  28554  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  mbfresfi  28576  ftc1cnnc  28604  ftc1anclem6  28610  dvasin  28618  trer  28649  clsun  28661  opnregcld  28663  cldregopn  28664  ssref  28693  fnessref  28703  fnopabco  28754  frinfm  28767  nninfnub  28785  caushft  28795  bndss  28823  ispridl2  28976  notornotel1  29036  tsbi2  29083  abeq12  29106  rabeq12f  29107  istopclsd  29174  pellex  29314  rmspecsqrnq  29385  monotoddzzfi  29421  jm2.23  29483  expdioph  29510  dford3lem1  29513  wopprc  29517  inisegn0  29534  kelac1  29554  dfac21  29557  lsmfgcl  29565  pwssplit4  29580  isnumbasgrp  29601  dgraalem  29640  pm10.12  29748  pm11.61  29784  sbiota1  29826  fnchoice  29889  fmuldfeq  29902  infrglb  29909  climsuselem1  29918  climsuse  29919  stoweidlem28  29961  stoweidlem52  29985  stoweidlem57  29990  wallispilem3  30000  wallispilem4  30001  wallispi  30003  wallispi2lem1  30004  wallispi2lem2  30005  wallispi2  30006  stirlinglem7  30013  stirlinglem10  30016  stirlinglem12  30018  dandysum2p2e4  30127  2reu4a  30151  ndmaovrcl  30248  pr1eqbg  30259  f12dfv  30284  f13dfv  30285  fvn0fvelrn  30291  el2fzo  30350  elfzonlteqm1  30363  hashrabsn01  30370  nbgrassvwo  30414  nbgrassvwo2  30415  uvtxnb  30416  usgra2wlkspthlem2  30435  usgra2pthlem1  30438  usgra2pth  30439  wwlknndef  30507  el2wlkonot  30526  el2spthonot  30527  el2wlkonotot0  30529  clwlkswlks  30561  clwwlknndef  30574  clwlkisclwwlklem2a4  30584  clwlkisclwwlklem1  30587  clwwlkf  30594  clwwlkvbij  30601  wwlkext2clwwlk  30603  clwwnisshclwwn  30611  erclwwlkref  30621  erclwwlknref  30637  erclwwlknsym  30638  erclwwlkntr  30639  hashecclwwlkn1  30646  usghashecclwwlk  30647  clwlkfoclwwlk  30656  wwlkextproplem3  30700  clwlknclwlkdifs  30716  frgra3v  30732  3vfriswmgra  30735  1to3vfriswmgra  30737  1to3vfriendship  30738  2pthfrgra  30741  4cycl2v2nb  30746  n4cyclfrgra  30748  frgranbnb  30750  frgrancvvdeqlem4  30764  frgrawopreg  30780  frg2woteqm  30790  usg2spot2nb  30796  numclwwlkovf2ex  30817  numclwwlk3lem  30839  fdmdifeqresdif  30870  altgsumbcALT  30888  lmod0rng  30917  fsuppmapnn0fiubex  30938  fsuppmapnn0fiub0  30939  ply1sclrmsm  30971  cply1mul  30993  lply1binom  30997  matsubgcell  31006  matinvgcell  31007  matvscacell  31009  mpt2matmul  31016  mat1dimbas  31022  scmatsubcl  31038  scmatmulcl  31040  lcoop  31052  lincfsuppcl  31054  linccl  31055  lincvalsng  31057  lincvalpr  31059  lincvalsc0  31062  linc0scn0  31064  lincdifsn  31065  linc1  31066  lincsum  31070  lincscm  31071  lindslinindsimp2lem5  31103  snlindsntor  31112  lincresunit3lem2  31121  ldepsnlinclem1  31154  ldepsnlinclem2  31155  pmatcoe1fsupp  31167  mat2pmatbas  31189  mat2pmatmul  31194  mat2pmatlin  31198  m2pminv2lem  31212  m2pminv2  31213  pmatcollpw1lem2  31224  pmatcollpw1dstlem1  31227  pmatcollpw1dst  31228  pmatcollpw1lem4  31230  pmatcollpw1lem5  31231  monmatcollpw  31236  pmatcollpw4  31240  pmatcollpw4fi  31241  pmattomply1f1  31267  pmattomply1ghm  31270  fvmptnn04ifb  31305  cayhamlem1  31320  cpmadumatpolylem3  31337  biimp  31485  bi2imp  31486  bi3impb  31487  bi3impa  31488  bi13impib  31490  bi123impib  31491  bi13impia  31492  bi123impia  31493  bi13imp23  31496  bi13imp2  31497  bi12imp3  31498  dfvd1imp  31588  dfvd2imp  31625  e1bi  31651  e2bi  31654  e3bi  31771  3ornot23VD  31883  3impexpbicomVD  31893  3impexpbicomiVD  31894  tratrbVD  31897  ssralv2VD  31902  equncomiVD  31905  truniALTVD  31914  ee33VD  31915  csbingVD  31920  onfrALTlem3VD  31923  onfrALTlem2VD  31925  onfrALTlem1VD  31926  onfrALTVD  31927  csbsngVD  31929  csbxpgVD  31930  csbrngVD  31932  csbunigVD  31934  csbfv12gALTVD  31935  relopabVD  31937  2uasbanhVD  31947  vk15.4jVD  31950  unisnALT  31962  chordthmALT  31969  iunconlem2  31971  bnj529  32033  bnj927  32062  bnj1379  32124  bnj1424  32132  bnj1436  32133  bnj1476  32140  bnj607  32209  bnj908  32224  bnj1097  32272  bnj1118  32275  bnj1128  32281  bnj1145  32284  bnj1154  32290  bnj1174  32294  bnj1189  32300  bnj1204  32303  bnj1388  32324  bnj1417  32332  sylancl2  32405  bj-babygodel  32423  bj-babylob  32424  bj-alrimhi  32455  bj-nfext  32502  bj-ax9  32699  bj-snsetex  32756  bj-1upln0  32802  bj-inftyexpidisj  32839  bj-elccinfty  32843  lkr0f  33045  glbconN  33327  paddssat  33764  pclunN  33848  2polssN  33865  paddunN  33877  poldmj1N  33878  ltrnnid  34086  dibglbN  35117
  Copyright terms: Public domain W3C validator