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  1254  syl3an2b  1255  syl3an3b  1256  nic-ax  1480  19.25  1658  sbbii  1707  spvw  1719  hbn1fw  1750  excomim  1788  stdpc5  1841  sb9i  2127  axc11n-16  2238  exmoeu  2287  exmoeuOLD  2288  2mo  2357  2moOLD  2358  2moOLDOLD  2359  eqeq1  2444  eleq2  2499  gencbvex  3011  moeq  3130  euind  3141  reuind  3157  eqsbc3r  3243  ssel  3345  unssd  3527  ssind  3569  n0moeu  3645  ss0  3663  uneqdifeq  3762  rabsnif  3939  prprc  3982  ssunsn2  4027  eqsn  4029  unisn2  4423  snexALT  4473  reusv3i  4494  snex  4528  brrelex12  4871  elrel  4937  exopxfr2  4979  dmxp  5053  xpssres  5139  elres  5140  elimasni  5191  xpdifid  5261  dmsnsnsn  5312  coi2  5349  xpco  5372  iotabi  5385  uniabio  5386  iotaint  5389  nfunv  5444  funun  5455  funcnv3  5474  funimass1  5486  funssxp  5566  f0dom0  5590  f1o00  5668  dffv3  5682  dffv2  5759  fndmin  5805  iinpreima  5828  fsn2  5878  ftpg  5887  fnsuppeq0OLD  5934  nvocnv  5983  isoselem  6027  riotaxfrd  6078  oprabid  6110  mpt2difsnif  6178  ovima0  6237  sorpsscmpl  6366  unexg  6376  ordsson  6396  peano2  6491  1stval  6574  2ndval  6575  1stdm  6616  oprabco  6652  f1o2ndf1  6675  poxp  6679  suppval1  6691  funsssuppss  6710  fnsuppeq0  6712  imacosupp  6724  tz7.49c  6893  undifixp  7291  bren2  7332  ensym  7350  en1uniel  7373  domunsn  7453  limenpsi  7478  php4  7490  isinf  7518  en2  7540  findcard2  7544  unfilem1  7568  suppssfifsupp  7627  fsuppunbi  7633  elfiun  7672  marypha1lem  7675  marypha2lem3  7679  supval2  7697  supmaxlem  7706  brwdom2  7780  brwdom3  7789  sucprcreg  7806  preleq  7815  tcmin  7953  prwf  8010  r1pw  8044  rankuni2b  8052  rankr1id  8061  cardval3  8114  ficardom  8123  cardmin2  8160  isinfcard  8254  iscard3  8255  alephval3  8272  dfac9  8297  kmlem6  8316  ackbij1lem12  8392  fin23lem29  8502  fin23lem30  8503  fin23lem41  8513  isf32lem11  8524  isfin1-3  8547  fin1a2lem11  8571  fin1a2lem12  8572  fin1a2lem13  8573  axcc2lem  8597  dominf  8606  axdc4lem  8616  dominfac  8729  pwcfsdom  8739  cfpwsdom  8740  tskuni  8942  wfgru  8975  rpregt0  10996  supxrun  11270  elfz1end  11471  1fv  11524  fzennn  11782  cardfz  11784  ser0  11850  crreczi  11981  faclbnd  12058  bcn1  12081  hashge0  12142  hashssdif  12159  hashsnlei  12162  euhash1  12164  hash2prd  12173  hashpw  12190  swrd0len0  12321  addlenrevswrd  12322  swrdtrcfv  12329  swrdswrd  12346  swrdccatwrd  12354  swrdccatin2  12370  swrdccat3  12375  swrdccat3a  12377  repsundef  12401  cshwlen  12428  s4f1o  12520  sqr0  12723  cau3lem  12834  harmonic  13313  mertenslem2  13337  rpnnen2  13500  prmind2  13766  pceq0  13929  prmreclem6  13974  0ram  14073  ram0  14075  cshwsdisj  14117  cshwsiun  14118  ressbas2  14221  ressinbas  14226  mrcuni  14551  mreexexlem4d  14577  catpropd  14640  arwhoma  14905  joinfval  15163  meetfval  15177  clatlem  15273  lubun  15285  psssdm  15378  plusfeq  15421  grpissubg  15692  idrespermg  15907  symgextfv  15914  fvcosymgeq  15925  pmtrprfv3  15951  pmtr3ncomlem1  15970  psgnunilem4  15994  gsumzoppg  16430  gsum2dlem1  16451  gsum2dlem2  16452  gsum2d  16453  gsum2dOLD  16454  rngsrg  16673  staffn  16914  scafeq  16948  lbsexg  17225  lidldvgen  17317  ply1bascl2  17640  prmirred  17899  prmirredOLD  17902  zlmassa  17935  frgpcyg  17986  ipfeq  18059  dsmmbas2  18142  frlmbas3  18181  mamufacex  18269  matepmcl  18327  matepm2cl  18328  marrepcl  18355  marepvcl  18360  mulmarep1el  18363  mulmarep1gsum1  18364  mulmarep1gsum2  18365  submabas  18369  nfimdetndef  18380  mdetfval1  18381  mdetunilem7  18404  mdetunilem9  18406  m2detleib  18417  gsummatr01lem3  18443  smadiadetlem4  18455  slesolinv  18466  slesolinvbi  18467  slesolex  18468  cramerimplem2  18470  isbasis3g  18534  isopn2  18616  ntrval2  18635  toponmre  18677  innei  18709  restcld  18756  restcldi  18757  neitr  18764  discmp  18981  cmpsublem  18982  cmpsub  18983  2ndcctbss  19039  ptcnp  19175  imasnopn  19243  imasncld  19244  imasncls  19245  kqf  19300  fbun  19393  opnfbas  19395  supfil  19448  ufprim  19462  acufl  19470  filufint  19473  ufldom  19515  hausflf2  19551  alexsubALTlem4  19602  cnextfval  19614  cnextfun  19616  cnextfres  19620  trust  19784  utoptop  19789  ustuqtop1  19796  metustidOLD  20114  metustid  20115  metustfbasOLD  20120  metustfbas  20121  cfilucfilOLD  20124  cfilucfil  20125  metustblOLD  20135  metustbl  20136  restmetu  20142  zlmclm  20647  cphassr  20710  ovolun  20962  volun  21006  vitalilem2  21069  dvmptfsum  21427  rolle  21442  ulmcaulem  21839  logfac  22029  logno1  22061  logreclem  22194  leibpilem1  22315  prmorcht  22496  pclogsum  22534  2sqlem10  22693  chto1lb  22707  tgldimor  22935  ncolne2  23013  axcontlem7  23184  ausisusgra  23247  usgra2edg1  23270  usgrarnedg  23271  usgraedg4  23273  usgra1v  23276  usgraidx2vlem2  23278  usgraidx2v  23279  usgrares1  23291  nb3graprlem2  23328  nb3grapr  23329  nb3grapr2  23330  nb3gra2nb  23331  cusgra3v  23340  cusgrafilem2  23356  usgrasscusgra  23359  uvtxnbgra  23369  2trllemH  23419  2trllemE  23420  constr1trl  23455  fargshiftfo  23492  vdgrnn0pnf  23547  eupatrl  23557  grpoidinvlem3  23661  nmlno0lem  24161  blocni  24173  pythi  24218  normpythi  24512  shmodsi  24760  omlsilem  24773  pjchi  24803  chlubii  24843  osumi  25013  nmlnop0iALT  25367  cnlnssadj  25452  nmopcoi  25467  mdbr3  25669  mdbr4  25670  ssmd1  25683  dmdsl3  25687  mdslmd1lem2  25698  mdslmd4i  25705  mdexchi  25707  atssma  25750  atoml2i  25755  chirredlem3  25764  mdsymlem1  25775  mdsymlem3  25777  dmdbr6ati  25795  dmdbr7ati  25796  cdjreui  25804  cdj3lem2b  25809  addltmulALT  25818  ssrmo  25846  iundifdif  25881  imadifxp  25907  fimacnvinrn2  25921  sspreima  25930  disjdsct  25966  resf1o  25998  fpwrelmap  26001  xlt2addrd  26019  xrge0infss  26021  ressmulgnn0  26113  xrge0neqmnf  26120  xrge0nre  26121  gsummpt2co  26217  kerunit  26259  pstmfval  26292  mndpluscn  26325  rge0scvg  26348  pnfneige0  26350  pl1cn  26354  nexple  26417  indval2  26440  gsumesum  26479  esumcst  26483  pwsiga  26542  insiga  26549  elsigagen2  26560  measxun2  26593  ddemeas  26621  aean  26629  mbfmfun  26638  mbfmbfm  26642  1stmbfm  26644  2ndmbfm  26645  oms0  26679  sibfof  26695  eulerpartlemt  26723  eulerpartlemmf  26727  eulerpartlemgs2  26732  probun  26771  dstfrvclim1  26829  coinfliprv  26834  ballotlem2  26840  ballotlemfp1  26843  ballotlemic  26858  ballotlem1c  26859  plymulx0  26917  signsvtn0  26940  signstres  26945  cvmliftlem10  27152  ghomgrpilem2  27274  prodf1  27375  fprodfac  27452  risefacp1  27501  fallfacp1  27502  faclim  27521  dfon2lem3  27567  dfon2lem7  27571  dfon2lem8  27572  rdgprc0  27576  wfrlem4  27696  wfrlem5  27697  wfrlem10  27702  wfrlem15  27707  frrlem4  27740  frrlem5  27741  fvsingle  27920  unisnif  27925  funpartlem  27942  hfun  28185  df3nandALT1  28212  lukshef-ax2  28231  nandsym1  28238  wl-lem-mo-recur  28364  finixpnum  28385  fin2so  28387  mblfinlem2  28400  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  mbfresfi  28409  ftc1cnnc  28437  ftc1anclem6  28443  dvasin  28451  trer  28482  clsun  28494  opnregcld  28496  cldregopn  28497  ssref  28526  fnessref  28536  fnopabco  28587  frinfm  28600  nninfnub  28618  caushft  28628  bndss  28656  ispridl2  28809  notornotel1  28869  tsbi2  28916  abeq12  28939  rabeq12f  28940  istopclsd  29007  pellex  29147  rmspecsqrnq  29218  monotoddzzfi  29254  jm2.23  29316  expdioph  29343  dford3lem1  29346  wopprc  29350  inisegn0  29367  kelac1  29387  dfac21  29390  lsmfgcl  29398  pwssplit4  29413  isnumbasgrp  29434  dgraalem  29473  pm10.12  29581  pm11.61  29617  sbiota1  29659  fnchoice  29722  fmuldfeq  29735  infrglb  29742  climsuselem1  29751  climsuse  29752  stoweidlem28  29794  stoweidlem52  29818  stoweidlem57  29823  wallispilem3  29833  wallispilem4  29834  wallispi  29836  wallispi2lem1  29837  wallispi2lem2  29838  wallispi2  29839  stirlinglem7  29846  stirlinglem10  29849  stirlinglem12  29851  dandysum2p2e4  29960  2reu4a  29984  ndmaovrcl  30081  pr1eqbg  30092  f12dfv  30117  f13dfv  30118  fvn0fvelrn  30124  el2fzo  30183  elfzonlteqm1  30196  hashrabsn01  30203  nbgrassvwo  30247  nbgrassvwo2  30248  uvtxnb  30249  usgra2wlkspthlem2  30268  usgra2pthlem1  30271  usgra2pth  30272  wwlknndef  30340  el2wlkonot  30359  el2spthonot  30360  el2wlkonotot0  30362  clwlkswlks  30394  clwwlknndef  30407  clwlkisclwwlklem2a4  30417  clwlkisclwwlklem1  30420  clwwlkf  30427  clwwlkvbij  30434  wwlkext2clwwlk  30436  clwwnisshclwwn  30444  erclwwlkref  30454  erclwwlknref  30470  erclwwlknsym  30471  erclwwlkntr  30472  hashecclwwlkn1  30479  usghashecclwwlk  30480  clwlkfoclwwlk  30489  wwlkextproplem3  30533  clwlknclwlkdifs  30549  frgra3v  30565  3vfriswmgra  30568  1to3vfriswmgra  30570  1to3vfriendship  30571  2pthfrgra  30574  4cycl2v2nb  30579  n4cyclfrgra  30581  frgranbnb  30583  frgrancvvdeqlem4  30597  frgrawopreg  30613  frg2woteqm  30623  usg2spot2nb  30629  numclwwlkovf2ex  30650  numclwwlk3lem  30672  fdmdifeqresdif  30702  snnen2o  30708  altgsumbcALT  30719  lmod0rng  30748  fsuppmapnn0fiubex  30769  fsuppmapnn0fiub0  30770  ply1sclrmsm  30795  lply1binom  30811  matsubgcell  30820  matvscacell  30821  mat1dimbas  30828  scmatsubcl  30844  scmatmulcl  30846  pmatcoe1fsupp  30852  pmatcollpw1lem2  30857  pmatcollpw1lem4  30859  pmatcollpw1lem5  30860  m1detdiag  30865  mdetdiag  30867  lcoop  30876  lincfsuppcl  30878  linccl  30879  lincvalsng  30881  lincvalpr  30883  lincvalsc0  30886  linc0scn0  30888  lincdifsn  30889  linc1  30890  lincsum  30894  lincscm  30895  lindslinindsimp2lem5  30927  snlindsntor  30936  lincresunit3lem2  30945  ldepsnlinclem1  30978  ldepsnlinclem2  30979  biimp  31114  bi2imp  31115  bi3impb  31116  bi3impa  31117  bi13impib  31119  bi123impib  31120  bi13impia  31121  bi123impia  31122  bi13imp23  31125  bi13imp2  31126  bi12imp3  31127  dfvd1imp  31217  dfvd2imp  31254  e1bi  31280  e2bi  31283  e3bi  31400  3ornot23VD  31512  3impexpbicomVD  31522  3impexpbicomiVD  31523  tratrbVD  31526  ssralv2VD  31531  equncomiVD  31534  truniALTVD  31543  ee33VD  31544  csbingVD  31549  onfrALTlem3VD  31552  onfrALTlem2VD  31554  onfrALTlem1VD  31555  onfrALTVD  31556  csbsngVD  31558  csbxpgVD  31559  csbrngVD  31561  csbunigVD  31563  csbfv12gALTVD  31564  relopabVD  31566  2uasbanhVD  31576  vk15.4jVD  31579  unisnALT  31591  chordthmALT  31598  iunconlem2  31600  bnj529  31662  bnj927  31691  bnj1379  31753  bnj1424  31761  bnj1436  31762  bnj1476  31769  bnj607  31838  bnj908  31853  bnj1097  31901  bnj1118  31904  bnj1128  31910  bnj1145  31913  bnj1154  31919  bnj1174  31923  bnj1189  31929  bnj1204  31932  bnj1388  31953  bnj1417  31961  sylancl2  32032  bj-babygodel  32044  bj-babylob  32045  bj-alrimhi  32076  bj-ax9  32299  bj-snsetex  32356  bj-1upln0  32402  bj-inftyexpidisj  32433  bj-elccinfty  32437  lkr0f  32632  glbconN  32914  paddssat  33351  pclunN  33435  2polssN  33452  paddunN  33464  poldmj1N  33465  ltrnnid  33673  dibglbN  34704
  Copyright terms: Public domain W3C validator