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

Theorem anidms 645
Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
anidms.1  |-  ( (
ph  /\  ph )  ->  ps )
Assertion
Ref Expression
anidms  |-  ( ph  ->  ps )

Proof of Theorem anidms
StepHypRef Expression
1 anidms.1 . . 3  |-  ( (
ph  /\  ph )  ->  ps )
21ex 434 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 47 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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  df-an 371
This theorem is referenced by:  sylancb  665  sylancbr  666  dedth2v  3866  dedth3v  3867  dedth4v  3868  intsng  4184  pwnss  4478  snex  4554  isso2i  4694  posn  4928  xpid11  5082  f1oprswap  5701  residpr  5907  f1mpt  5995  f1eqcocnv  6020  isopolem  6057  resiexg  6535  poxp  6705  oe0  6983  oecl  6998  nnmsucr  7085  erex  7146  ecopover  7225  enrefg  7362  php  7516  dffi3  7702  hartogslem2  7778  harwdom  7826  infxpenlem  8201  dfac8b  8222  ac10ct  8225  xp2cda  8370  isfin5-2  8581  fpwwe2lem5  8822  canthwe  8839  pwfseqlem4a  8849  pwfseqlem4  8850  pwfseqlem5  8851  pwfseq  8852  nqereu  9119  halfnq  9166  ltsopr  9222  1idsr  9286  00sr  9287  sqgt0sr  9294  leid  9491  msqgt0  9881  msqge0  9882  recextlem1  9987  recextlem2  9988  recex  9989  div1  10044  cju  10339  2halves  10574  msqznn  10744  uzindOLD  10757  xrltnr  11122  xrleid  11148  iccid  11366  expubnd  11945  sqneg  11947  sqcl  11949  nnsqcl  11956  qsqcl  11958  subsq2  11995  bernneq  12011  faclbnd  12087  faclbnd3  12089  hashfac  12232  leiso  12233  cjmulval  12655  sin2t  13482  cos2t  13483  divalglem0  13618  divalglem2  13620  gcd0id  13728  isprm5  13819  ssclem  14753  prslem  15122  ipolerval  15347  pslem  15397  dirref  15426  grpsubid  15631  cntzi  15868  symgval  15905  symgbas  15906  symgbasfi  15912  symg1bas  15922  pgrpsubgsymg  15934  symgextfve  15945  pmtrfinv  15988  lsmidm  16182  ipeq0  18089  mamulid  18326  mamurid  18327  mat0op  18342  matsca2  18343  matbas2  18344  matecl  18348  matlmod  18351  mattposcl  18359  mattposvs  18361  mdetunilem9  18448  idcn  18883  hausdiag  19240  symgtgp  19694  ustval  19799  isust  19800  ustref  19815  ustelimasn  19819  restutopopn  19835  ressuss  19860  iducn  19880  ispsmet  19902  ismet  19920  isxmet  19921  idnghm  20344  resubmet  20401  xrsxmet  20408  cphnm  20734  tchnmval  20766  ipcau2  20771  tchcphlem1  20772  tchcphlem2  20773  tchcph  20774  chordthmlem  22249  resgrprn  23789  ismgm  23829  opidon2  23833  rngo2  23897  vcoprnelem  23978  hmoval  24232  htth  24342  hvsubid  24450  hvnegid  24451  hv2times  24485  hiidrcl  24519  normval  24548  issh2  24633  chjidm  24945  normcan  25001  ho2times  25245  kbpj  25382  lnop0  25392  riesz3i  25488  leoprf  25554  leopsq  25555  cvnref  25717  gtiso  26018  prsss  26368  ordtrestNEW  26373  deranglem  27076  m1expevenALT  27129  fallrisefac  27550  dfpo2  27587  predpoirr  27680  predfrirr  27681  elfix2  27957  linedegen  28196  fin2so  28442  ftc1anclem3  28495  filnetlem2  28626  prdsbnd2  28720  reheibor  28764  exidreslem  28768  mzpf  29098  acongrep  29349  ttac  29411  mendval  29566  mendplusgfval  29568  mendmulrfval  29570  iocinico  29613  iocmbl  29614  seff  29621  sblpnf  29622  sigarid  29920  3xpexg  30146  3xpfi  30192  cnambpcma  30194  2leaddle2  30201  is2wlkonot  30408  is2spthonot  30409  2wlkonot  30410  2spthonot  30411  2spotfi  30437  2spotmdisj  30687  f1o2sn  30752  psgnsn  30801  matplusgcell  30895  matsubgcell  30896  mat1dimelbas  30906  mat1dimscm  30910  m1detdiag  30931  mdetdiagid  30934  d1mat2pmat  31090  pmatcoe1fsupp  31107  bj-ru0  32531
  Copyright terms: Public domain W3C validator