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  3995  dedth3v  3996  dedth4v  3997  intsng  4317  pwnss  4612  snex  4688  isso2i  4832  posn  5068  xpid11  5224  f1oprswap  5855  f1o2sn  6064  residpr  6065  f1mpt  6157  f1eqcocnv  6192  isopolem  6229  3xpexg  6587  sqxpexg  6589  resiexg  6720  poxp  6895  oe0  7172  oecl  7187  nnmsucr  7274  erex  7335  ecopover  7415  enrefg  7547  php  7701  3xpfi  7792  dffi3  7891  hartogslem2  7968  harwdom  8016  infxpenlem  8391  dfac8b  8412  ac10ct  8415  xp2cda  8560  isfin5-2  8771  fpwwe2lem5  9012  canthwe  9029  pwfseqlem4a  9039  pwfseqlem4  9040  pwfseqlem5  9041  pwfseq  9042  nqereu  9307  halfnq  9354  ltsopr  9410  1idsr  9475  00sr  9476  sqgt0sr  9483  leid  9680  msqgt0  10073  msqge0  10074  recextlem1  10179  recextlem2  10180  recex  10181  div1  10236  cju  10532  2halves  10767  msqznn  10942  uzindOLD  10955  xrltnr  11330  xrleid  11356  iccid  11574  expubnd  12194  sqneg  12196  sqcl  12198  nnsqcl  12205  qsqcl  12207  subsq2  12244  bernneq  12260  faclbnd  12336  faclbnd3  12338  hashfac  12473  leiso  12474  cjmulval  12941  sin2t  13773  cos2t  13774  divalglem0  13910  divalglem2  13912  gcd0id  14020  isprm5  14112  ssclem  15049  prslem  15418  ipolerval  15643  pslem  15693  dirref  15722  grpsubid  15932  cntzi  16172  symgval  16209  symgbas  16210  symgbasfi  16216  symg1bas  16226  pgrpsubgsymg  16238  symgextfve  16249  pmtrfinv  16292  psgnsn  16351  lsmidm  16488  ipeq0  18468  mat0op  18716  matsca2  18717  matbas2  18718  matecl  18722  matlmod  18726  matplusgcell  18730  matsubgcell  18731  mamulid  18738  mamurid  18739  mattposcl  18750  mattposvs  18752  mat1dimelbas  18768  mat1dimscm  18772  m1detdiag  18894  mdetdiagid  18897  mdetunilem9  18917  pmatcoe1fsupp  18997  d1mat2pmat  19035  idcn  19552  hausdiag  19909  symgtgp  20363  ustval  20468  isust  20469  ustref  20484  ustelimasn  20488  restutopopn  20504  ressuss  20529  iducn  20549  ispsmet  20571  ismet  20589  isxmet  20590  idnghm  21013  resubmet  21070  xrsxmet  21077  cphnm  21403  tchnmval  21435  ipcau2  21440  tchcphlem1  21441  tchcphlem2  21442  tchcph  21443  chordthmlem  22919  ismot  23678  is2wlkonot  24567  is2spthonot  24568  2wlkonot  24569  2spthonot  24570  2spotfi  24596  2spotmdisj  24773  resgrprn  24986  ismgm  25026  opidon2  25030  rngo2  25094  vcoprnelem  25175  hmoval  25429  htth  25539  hvsubid  25647  hvnegid  25648  hv2times  25682  hiidrcl  25716  normval  25745  issh2  25830  chjidm  26142  normcan  26198  ho2times  26442  kbpj  26579  lnop0  26589  riesz3i  26685  leoprf  26751  leopsq  26752  cvnref  26914  gtiso  27219  prsss  27562  ordtrestNEW  27567  deranglem  28278  m1expevenALT  28331  fallrisefac  28752  dfpo2  28789  predpoirr  28882  predfrirr  28883  elfix2  29159  linedegen  29398  fin2so  29645  ftc1anclem3  29697  filnetlem2  29828  prdsbnd2  29922  reheibor  29966  exidreslem  29970  mzpf  30300  acongrep  30550  ttac  30610  mendval  30765  mendplusgfval  30767  mendmulrfval  30769  iocinico  30812  iocmbl  30813  seff  30820  sblpnf  30821  lcmid  30843  lcmgcdeq  30844  sigarid  31570  cnambpcma  31810  2leaddle2  31815  clintopval  31984  bj-ru0  33599
  Copyright terms: Public domain W3C validator