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  3623  dedth3v  3624  dedth4v  3625  intsng  3913  pwnss  4192  snex  4232  isso2i  4362  posn  4774  xpid11  4916  resiexg  5013  f1oprswap  5531  f1mpt  5801  f1eqcocnv  5821  isopolem  5858  poxp  6243  oe0  6537  oecl  6552  nnmsucr  6639  erex  6700  ecopover  6778  enrefg  6909  php  7061  dffi3  7200  hartogslem2  7274  harwdom  7320  infxpenlem  7657  dfac8b  7674  ac10ct  7677  xp2cda  7822  isfin5-2  8033  fpwwe2lem5  8272  canthwe  8289  pwfseqlem4a  8299  pwfseqlem4  8300  pwfseqlem5  8301  pwfseq  8302  nqereu  8569  halfnq  8616  ltsopr  8672  1idsr  8736  00sr  8737  sqgt0sr  8744  leid  8932  msqgt0  9310  msqge0  9311  recextlem1  9414  recextlem2  9415  recex  9416  div1  9469  cju  9758  2halves  9956  msqznn  10109  uzindOLD  10122  xrltnr  10478  xrleid  10500  iccid  10717  expubnd  11178  sqneg  11180  sqcl  11182  nnsqcl  11189  qsqcl  11191  subsq2  11227  bernneq  11243  faclbnd  11319  faclbnd3  11321  hashfac  11412  leiso  11413  cjmulval  11646  sin2t  12473  cos2t  12474  divalglem0  12608  divalglem2  12610  gcd0id  12718  isprm5  12807  ssclem  13712  isfull  13800  isfth  13804  prslem  14081  ipolerval  14275  pslem  14331  dirref  14373  grpsubid  14566  symgval  14787  symgbas  14788  cntzi  14821  lsmidm  14989  ipeq0  16558  idcn  17003  hausdiag  17355  symgtgp  17800  ismet  17904  isxmet  17905  idnghm  18268  resubmet  18324  xrsxmet  18331  cphnm  18645  tchnmval  18676  ipcau2  18680  tchcphlem1  18681  tchcphlem2  18682  tchcph  18683  chordthmlem  20145  resgrprn  20963  ismgm  21003  opidon2  21007  rngo2  21071  vcoprnelem  21150  hmoval  21404  htth  21514  hvsubid  21621  hvnegid  21622  hv2times  21656  hiidrcl  21690  normval  21719  issh2  21804  chjidm  22115  normcan  22171  ho2times  22415  kbpj  22552  lnop0  22562  riesz3i  22658  leoprf  22724  leopsq  22725  cvnref  22887  gtiso  23256  deranglem  23712  dfpo2  24183  predpoirr  24268  predfrirr  24269  elfix2  24515  linedegen  24838  domintreflemb  25165  cnvref  25168  islatalg  25286  jidd  25295  midd  25296  preoref22  25332  sqpre  25341  inposet  25381  ridlideq  25438  rzrlzreq  25439  svs2  25590  hmeogrp  25640  mslb1  25710  distmlva  25791  icccon2  25803  idfisf  25944  catsbc  25952  prismorcsetlem  26015  prismorcset  26017  idmor  26049  codidmor  26053  filnetlem2  26431  prdsbnd2  26622  reheibor  26666  exidreslem  26670  mzpf  26917  acongrep  27170  ttac  27232  pmtrfinv  27505  mamulid  27561  mamurid  27562  matsca2  27577  matbas2  27578  matlmod  27582  mendval  27594  mendplusgfval  27596  mendmulrfval  27598  seff  27641  sblpnf  27642  sigarid  27951  eel011  28787
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