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  3978  dedth3v  3979  dedth4v  3980  intsng  4303  pwnss  4598  snex  4674  isso2i  4818  posn  5054  xpid11  5210  f1oprswap  5841  f1o2sn  6055  residpr  6056  f1mpt  6150  f1eqcocnv  6185  isopolem  6222  3xpexg  6584  sqxpexg  6586  poxp  6893  oe0  7170  oecl  7185  nnmsucr  7272  ecopover  7413  enrefg  7545  php  7699  3xpfi  7790  dffi3  7889  infxpenlem  8389  xp2cda  8558  isfin5-2  8769  fpwwe2lem5  9010  pwfseqlem4a  9037  pwfseqlem4  9038  pwfseqlem5  9039  pwfseq  9040  nqereu  9305  halfnq  9352  ltsopr  9408  1idsr  9473  00sr  9474  sqgt0sr  9481  leid  9678  msqgt0  10074  msqge0  10075  recextlem1  10180  recextlem2  10181  recex  10182  div1  10237  cju  10533  2halves  10768  msqznn  10945  uzindOLD  10958  xrltnr  11334  xrleid  11360  iccid  11578  expubnd  12200  sqneg  12202  sqcl  12204  nnsqcl  12211  qsqcl  12213  subsq2  12250  bernneq  12266  faclbnd  12342  faclbnd3  12344  hashfac  12481  leiso  12482  cjmulval  12952  sin2t  13784  cos2t  13785  divalglem0  13923  divalglem2  13925  gcd0id  14033  isprm5  14125  prslem  15429  pslem  15705  dirref  15734  sgrp2nmndlem4  15915  grpsubid  15991  cntzi  16236  symgval  16273  symgbas  16274  symgbasfi  16280  symg1bas  16290  pgrpsubgsymg  16302  symgextfve  16313  pmtrfinv  16355  psgnsn  16414  lsmidm  16551  ipeq0  18540  matsca2  18789  matbas2  18790  matplusgcell  18802  matsubgcell  18803  mamulid  18810  mamurid  18811  mattposcl  18822  mat1dimelbas  18840  mat1dimscm  18844  m1detdiag  18966  mdetdiagid  18969  mdetunilem9  18989  pmatcoe1fsupp  19069  d1mat2pmat  19107  idcn  19624  hausdiag  20012  symgtgp  20466  ustref  20587  ustelimasn  20591  iducn  20652  ismet  20692  isxmet  20693  idnghm  21116  resubmet  21173  xrsxmet  21180  cphnm  21506  tchnmval  21538  ipcau2  21543  tchcphlem1  21544  tchcphlem2  21545  tchcph  21546  chordthmlem  23028  ismot  23787  is2wlkonot  24728  is2spthonot  24729  resgrprn  25147  ismgmOLD  25187  opidon2OLD  25191  rngo2  25255  vcoprnelem  25336  hmoval  25590  htth  25700  hvsubid  25808  hvnegid  25809  hv2times  25843  hiidrcl  25877  normval  25906  issh2  25991  chjidm  26303  normcan  26359  ho2times  26603  kbpj  26740  lnop0  26750  riesz3i  26846  leoprf  26912  leopsq  26913  cvnref  27075  gtiso  27384  prsss  27764  deranglem  28476  m1expevenALT  28529  fallrisefac  29115  dfpo2  29152  predpoirr  29245  predfrirr  29246  elfix2  29522  linedegen  29761  ftc1anclem3  30060  filnetlem2  30165  prdsbnd2  30259  reheibor  30303  exidreslem  30307  mzpf  30636  acongrep  30886  ttac  30946  mendval  31101  mendplusgfval  31103  mendmulrfval  31105  iocinico  31148  iocmbl  31149  seff  31158  sblpnf  31159  lcmid  31184  lcmgcdeq  31185  sigarid  31909  cnambpcma  32149  2leaddle2  32154  clintopval  32361  bj-ru0  34212
  Copyright terms: Public domain W3C validator