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, 5-Aug-1993.)
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  457  simprbi  461  sylanb  469  sylan2b  472  pm3.1  495  orbi2i  516  pm2.32  523  anc2l  550  pm3.37  574  dfbi  622  pm2.76  837  pm5.15  877  pm5.16  878  pm5.75  921  rnlem  949  simp1bi  996  simp2bi  997  simp3bi  998  syl3an1b  1247  syl3an2b  1248  syl3an3b  1249  nic-ax  1483  19.25  1657  sbbii  1706  spvw  1718  hbn1fw  1749  excomim  1787  stdpc5  1839  sb9i  2129  axc11n-16  2240  exmoeu  2286  exmoeuOLD  2287  2mo  2355  2moOLD  2356  eqeq1  2439  eleq2  2494  gencbvex  3005  moeq  3124  euind  3135  reuind  3151  eqsbc3r  3236  ssel  3338  unssd  3520  ssind  3562  n0moeu  3638  ss0  3656  uneqdifeq  3755  rabsnif  3932  prprc  3975  ssunsn2  4020  eqsn  4022  unisn2  4416  snexALT  4466  reusv3i  4487  snex  4521  brrelex12  4863  elrel  4929  exopxfr2  4971  dmxp  5045  xpssres  5132  elres  5133  elimasni  5184  xpdifid  5254  dmsnsnsn  5305  coi2  5342  xpco  5365  iotabi  5378  uniabio  5379  iotaint  5382  nfunv  5437  funun  5448  funcnv3  5467  funimass1  5479  funssxp  5559  f0dom0  5583  f1o00  5661  dffv3  5675  dffv2  5752  fndmin  5798  iinpreima  5821  fsn2  5870  ftpg  5879  fnsuppeq0OLD  5926  nvocnv  5975  isoselem  6019  riotaxfrd  6071  oprabid  6104  mpt2difsnif  6172  ovima0  6231  sorpsscmpl  6360  unexg  6370  ordsson  6390  peano2  6485  1stval  6568  2ndval  6569  1stdm  6610  oprabco  6646  f1o2ndf1  6669  poxp  6673  suppval1  6685  funsssuppss  6704  fnsuppeq0  6706  imacosupp  6718  tz7.49c  6887  undifixp  7287  bren2  7328  ensym  7346  en1uniel  7369  domunsn  7449  limenpsi  7474  php4  7486  isinf  7514  en2  7536  findcard2  7540  unfilem1  7564  suppssfifsupp  7623  fsuppunbi  7629  elfiun  7668  marypha1lem  7671  marypha2lem3  7675  supval2  7693  supmaxlem  7702  brwdom2  7776  brwdom3  7785  sucprcreg  7802  preleq  7811  tcmin  7949  prwf  8006  r1pw  8040  rankuni2b  8048  rankr1id  8057  cardval3  8110  ficardom  8119  cardmin2  8156  isinfcard  8250  iscard3  8251  alephval3  8268  dfac9  8293  kmlem6  8312  ackbij1lem12  8388  fin23lem29  8498  fin23lem30  8499  fin23lem41  8509  isf32lem11  8520  isfin1-3  8543  fin1a2lem11  8567  fin1a2lem12  8568  fin1a2lem13  8569  axcc2lem  8593  dominf  8602  axdc4lem  8612  dominfac  8725  pwcfsdom  8735  cfpwsdom  8736  tskuni  8937  wfgru  8970  rpregt0  10991  supxrun  11265  elfz1end  11465  1fv  11515  fzennn  11773  cardfz  11775  ser0  11841  crreczi  11972  faclbnd  12049  bcn1  12072  hashge0  12133  hashssdif  12150  hashsnlei  12153  euhash1  12155  hash2prd  12164  hashpw  12181  swrd0len0  12312  addlenrevswrd  12313  swrdtrcfv  12320  swrdswrd  12337  swrdccatwrd  12345  swrdccatin2  12361  swrdccat3  12366  swrdccat3a  12368  repsundef  12392  cshwlen  12419  s4f1o  12511  sqr0  12714  cau3lem  12825  harmonic  13303  mertenslem2  13327  rpnnen2  13490  prmind2  13756  pceq0  13919  prmreclem6  13964  0ram  14063  ram0  14065  cshwsdisj  14107  cshwsiun  14108  ressbas2  14211  ressinbas  14216  mrcuni  14541  mreexexlem4d  14567  catpropd  14630  arwhoma  14895  joinfval  15153  meetfval  15167  clatlem  15263  lubun  15275  psssdm  15368  plusfeq  15411  grpissubg  15680  idrespermg  15895  symgextfv  15902  fvcosymgeq  15913  pmtrprfv3  15939  pmtr3ncomlem1  15958  psgnunilem4  15982  gsumzoppg  16415  gsum2dlem1  16434  gsum2dlem2  16435  gsum2d  16436  gsum2dOLD  16437  staffn  16857  scafeq  16891  lbsexg  17166  lidldvgen  17258  ply1bascl2  17558  prmirred  17760  prmirredOLD  17763  zlmassa  17796  frgpcyg  17847  ipfeq  17920  dsmmbas2  18003  frlmbas3  18042  mamufacex  18130  matepmcl  18188  matepm2cl  18189  marrepcl  18216  marepvcl  18221  mulmarep1el  18224  mulmarep1gsum1  18225  mulmarep1gsum2  18226  submabas  18230  nfimdetndef  18241  mdetfval1  18242  mdetunilem7  18265  mdetunilem9  18267  m2detleib  18278  gsummatr01lem3  18304  smadiadetlem4  18316  slesolinv  18327  slesolinvbi  18328  slesolex  18329  cramerimplem2  18331  isbasis3g  18395  isopn2  18477  ntrval2  18496  toponmre  18538  innei  18570  restcld  18617  restcldi  18618  neitr  18625  discmp  18842  cmpsublem  18843  cmpsub  18844  2ndcctbss  18900  ptcnp  19036  imasnopn  19104  imasncld  19105  imasncls  19106  kqf  19161  fbun  19254  opnfbas  19256  supfil  19309  ufprim  19323  acufl  19331  filufint  19334  ufldom  19376  hausflf2  19412  alexsubALTlem4  19463  cnextfval  19475  cnextfun  19477  cnextfres  19481  trust  19645  utoptop  19650  ustuqtop1  19657  metustidOLD  19975  metustid  19976  metustfbasOLD  19981  metustfbas  19982  cfilucfilOLD  19985  cfilucfil  19986  metustblOLD  19996  metustbl  19997  restmetu  20003  zlmclm  20508  cphassr  20571  ovolun  20823  volun  20867  vitalilem2  20930  dvmptfsum  21288  rolle  21303  ulmcaulem  21743  logfac  21933  logno1  21965  logreclem  22098  leibpilem1  22219  prmorcht  22400  pclogsum  22438  2sqlem10  22597  chto1lb  22611  tgldimor  22836  axcontlem7  23038  ausisusgra  23101  usgra2edg1  23124  usgrarnedg  23125  usgraedg4  23127  usgra1v  23130  usgraidx2vlem2  23132  usgraidx2v  23133  usgrares1  23145  nb3graprlem2  23182  nb3grapr  23183  nb3grapr2  23184  nb3gra2nb  23185  cusgra3v  23194  cusgrafilem2  23210  usgrasscusgra  23213  uvtxnbgra  23223  2trllemH  23273  2trllemE  23274  constr1trl  23309  fargshiftfo  23346  vdgrnn0pnf  23401  eupatrl  23411  grpoidinvlem3  23515  nmlno0lem  24015  blocni  24027  pythi  24072  normpythi  24366  shmodsi  24614  omlsilem  24627  pjchi  24657  chlubii  24697  osumi  24867  nmlnop0iALT  25221  cnlnssadj  25306  nmopcoi  25321  mdbr3  25523  mdbr4  25524  ssmd1  25537  dmdsl3  25541  mdslmd1lem2  25552  mdslmd4i  25559  mdexchi  25561  atssma  25604  atoml2i  25609  chirredlem3  25618  mdsymlem1  25629  mdsymlem3  25631  dmdbr6ati  25649  dmdbr7ati  25650  cdjreui  25658  cdj3lem2b  25663  addltmulALT  25672  ssrmo  25701  iundifdif  25736  imadifxp  25762  fimacnvinrn2  25776  sspreima  25785  disjdsct  25821  resf1o  25854  fpwrelmap  25857  xlt2addrd  25875  ressmulgnn0  25967  xrge0neqmnf  25974  xrge0nre  25975  rngsrg  26042  gsummpt2co  26100  kerunit  26143  pstmfval  26176  mndpluscn  26209  rge0scvg  26232  pnfneige0  26234  pl1cn  26238  nexple  26301  indval2  26324  gsumesum  26363  esumcst  26367  pwsiga  26426  insiga  26433  elsigagen2  26444  measxun2  26477  ddemeas  26505  aean  26513  mbfmfun  26522  mbfmbfm  26526  1stmbfm  26528  2ndmbfm  26529  sibfof  26573  eulerpartlemt  26601  eulerpartlemmf  26605  eulerpartlemgs2  26610  probun  26649  dstfrvclim1  26707  coinfliprv  26712  ballotlem2  26718  ballotlemfp1  26721  ballotlemic  26736  ballotlem1c  26737  plymulx0  26795  signsvtn0  26818  signstres  26823  cvmliftlem10  27030  ghomgrpilem2  27151  prodf1  27252  fprodfac  27329  risefacp1  27378  fallfacp1  27379  faclim  27398  dfon2lem3  27444  dfon2lem7  27448  dfon2lem8  27449  rdgprc0  27453  wfrlem4  27573  wfrlem5  27574  wfrlem10  27579  wfrlem15  27584  frrlem4  27617  frrlem5  27618  fvsingle  27797  unisnif  27802  funpartlem  27819  hfun  28062  df3nandALT1  28089  lukshef-ax2  28108  nandsym1  28115  finixpnum  28255  fin2so  28257  mblfinlem2  28270  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  mbfresfi  28279  ftc1cnnc  28307  ftc1anclem6  28313  dvasin  28321  trer  28352  clsun  28364  opnregcld  28366  cldregopn  28367  ssref  28396  fnessref  28406  fnopabco  28457  frinfm  28470  nninfnub  28488  caushft  28498  bndss  28526  ispridl2  28679  notornotel1  28739  tsbi2  28786  abeq12  28809  rabeq12f  28810  istopclsd  28878  pellex  29018  rmspecsqrnq  29089  monotoddzzfi  29125  jm2.23  29187  expdioph  29214  dford3lem1  29217  wopprc  29221  inisegn0  29238  kelac1  29258  dfac21  29261  lsmfgcl  29269  pwssplit4  29284  isnumbasgrp  29305  dgraalem  29344  pm10.12  29452  pm11.61  29488  sbiota1  29530  fnchoice  29593  fmuldfeq  29606  infrglb  29614  climsuselem1  29623  climsuse  29624  stoweidlem28  29666  stoweidlem52  29690  stoweidlem57  29695  wallispilem3  29705  wallispilem4  29706  wallispi  29708  wallispi2lem1  29709  wallispi2lem2  29710  wallispi2  29711  stirlinglem7  29718  stirlinglem10  29721  stirlinglem12  29723  dandysum2p2e4  29832  2reu4a  29856  ndmaovrcl  29953  pr1eqbg  29964  f12dfv  29989  f13dfv  29990  fvn0fvelrn  29996  el2fzo  30055  elfzonlteqm1  30068  hashrabsn01  30075  nbgrassvwo  30119  nbgrassvwo2  30120  uvtxnb  30121  usgra2wlkspthlem2  30140  usgra2pthlem1  30143  usgra2pth  30144  wwlknndef  30212  el2wlkonot  30231  el2spthonot  30232  el2wlkonotot0  30234  clwlkswlks  30266  clwwlknndef  30279  clwlkisclwwlklem2a4  30289  clwlkisclwwlklem1  30292  clwwlkf  30299  clwwlkvbij  30306  wwlkext2clwwlk  30308  clwwnisshclwwn  30316  erclwwlkref  30326  erclwwlknref  30342  erclwwlknsym  30343  erclwwlkntr  30344  hashecclwwlkn1  30351  usghashecclwwlk  30352  clwlkfoclwwlk  30361  wwlkextproplem3  30405  clwlknclwlkdifs  30421  frgra3v  30437  3vfriswmgra  30440  1to3vfriswmgra  30442  1to3vfriendship  30443  2pthfrgra  30446  4cycl2v2nb  30451  n4cyclfrgra  30453  frgranbnb  30455  frgrancvvdeqlem4  30469  frgrawopreg  30485  frg2woteqm  30495  usg2spot2nb  30501  numclwwlkovf2ex  30522  numclwwlk3lem  30544  fdmdifeqresdif  30573  snnen2o  30579  lmod0rng  30607  matsubgcell  30638  matvscacell  30639  lcoop  30651  lincfsuppcl  30653  linccl  30654  lincvalsng  30656  lincvalpr  30658  lincvalsc0  30661  linc0scn0  30663  lincdifsn  30664  linc1  30665  lincsum  30669  lincscm  30670  lindslinindsimp2lem5  30702  snlindsntor  30711  lincresunit3lem2  30720  ldepsnlinclem1  30753  ldepsnlinclem2  30754  biimp  30883  bi2imp  30884  bi3impb  30885  bi3impa  30886  bi13impib  30888  bi123impib  30889  bi13impia  30890  bi123impia  30891  bi13imp23  30894  bi13imp2  30895  bi12imp3  30896  dfvd1imp  30987  dfvd2imp  31024  e1bi  31050  e2bi  31053  e3bi  31170  3ornot23VD  31282  3impexpbicomVD  31292  3impexpbicomiVD  31293  tratrbVD  31296  ssralv2VD  31301  equncomiVD  31304  truniALTVD  31313  ee33VD  31314  csbingVD  31319  onfrALTlem3VD  31322  onfrALTlem2VD  31324  onfrALTlem1VD  31325  onfrALTVD  31326  csbsngVD  31328  csbxpgVD  31329  csbrngVD  31331  csbunigVD  31333  csbfv12gALTVD  31334  relopabVD  31336  2uasbanhVD  31346  vk15.4jVD  31349  unisnALT  31361  chordthmALT  31368  iunconlem2  31370  bnj529  31432  bnj927  31461  bnj1379  31523  bnj1424  31531  bnj1436  31532  bnj1476  31539  bnj607  31608  bnj908  31623  bnj1097  31671  bnj1118  31674  bnj1128  31680  bnj1145  31683  bnj1154  31689  bnj1174  31693  bnj1189  31699  bnj1204  31702  bnj1388  31723  bnj1417  31731  sylancl2  31770  bj-babygodel  31782  bj-babylob  31783  bj-alrimhi  31813  bj-ax9  31990  bj-snsetex  32036  bj-1upln0  32082  bj-inftyexpidisj  32110  bj-elccinfty  32114  lkr0f  32309  glbconN  32591  paddssat  33028  pclunN  33112  2polssN  33129  paddunN  33141  poldmj1N  33142  ltrnnid  33350  dibglbN  34381
  Copyright terms: Public domain W3C validator