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

Theorem anidms 626
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 423 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 43 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylancb  646  sylancbr  647  dedth2v  3610  dedth3v  3611  dedth4v  3612  intsng  3897  pwnss  4176  snex  4216  isso2i  4346  posn  4758  xpid11  4900  resiexg  4997  f1oprswap  5515  f1mpt  5785  f1eqcocnv  5805  isopolem  5842  poxp  6227  oe0  6521  oecl  6536  nnmsucr  6623  erex  6684  ecopover  6762  enrefg  6893  php  7045  dffi3  7184  hartogslem2  7258  harwdom  7304  infxpenlem  7641  dfac8b  7658  ac10ct  7661  xp2cda  7806  isfin5-2  8017  fpwwe2lem5  8256  canthwe  8273  pwfseqlem4a  8283  pwfseqlem4  8284  pwfseqlem5  8285  pwfseq  8286  nqereu  8553  halfnq  8600  ltsopr  8656  1idsr  8720  00sr  8721  sqgt0sr  8728  leid  8916  msqgt0  9294  msqge0  9295  recextlem1  9398  recextlem2  9399  recex  9400  div1  9453  cju  9742  2halves  9940  msqznn  10093  uzindOLD  10106  xrltnr  10462  xrleid  10484  iccid  10701  expubnd  11162  sqneg  11164  sqcl  11166  nnsqcl  11173  qsqcl  11175  subsq2  11211  bernneq  11227  faclbnd  11303  faclbnd3  11305  hashfac  11396  leiso  11397  cjmulval  11630  sin2t  12457  cos2t  12458  divalglem0  12592  divalglem2  12594  gcd0id  12702  isprm5  12791  ssclem  13696  isfull  13784  isfth  13788  prslem  14065  ipolerval  14259  pslem  14315  dirref  14357  grpsubid  14550  symgval  14771  symgbas  14772  cntzi  14805  lsmidm  14973  ipeq0  16542  idcn  16987  hausdiag  17339  symgtgp  17784  ismet  17888  isxmet  17889  idnghm  18252  resubmet  18308  xrsxmet  18315  cphnm  18629  tchnmval  18660  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  tchcph  18667  chordthmlem  20129  resgrprn  20947  ismgm  20987  opidon2  20991  rngo2  21055  vcoprnelem  21134  hmoval  21388  htth  21498  hvsubid  21605  hvnegid  21606  hv2times  21640  hiidrcl  21674  normval  21703  issh2  21788  chjidm  22099  normcan  22155  ho2times  22399  kbpj  22536  lnop0  22546  riesz3i  22642  leoprf  22708  leopsq  22709  cvnref  22871  gtiso  23241  deranglem  23697  dfpo2  24112  predpoirr  24197  predfrirr  24198  elfix2  24444  linedegen  24766  domintreflemb  25062  cnvref  25065  islatalg  25183  jidd  25192  midd  25193  preoref22  25229  sqpre  25238  inposet  25278  ridlideq  25335  rzrlzreq  25336  svs2  25487  hmeogrp  25537  mslb1  25607  distmlva  25688  icccon2  25700  idfisf  25841  catsbc  25849  prismorcsetlem  25912  prismorcset  25914  idmor  25946  codidmor  25950  filnetlem2  26328  prdsbnd2  26519  reheibor  26563  exidreslem  26567  mzpf  26814  acongrep  27067  ttac  27129  pmtrfinv  27402  mamulid  27458  mamurid  27459  matsca2  27474  matbas2  27475  matlmod  27479  mendval  27491  mendplusgfval  27493  mendmulrfval  27495  seff  27538  sblpnf  27539  sigarid  27848  eel011  28482
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator