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

Theorem anidms 680
Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
anidms.1 ((𝜑𝜑) → 𝜓)
Assertion
Ref Expression
anidms (𝜑𝜓)

Proof of Theorem anidms
StepHypRef Expression
1 anidms.1 . . 3 ((𝜑𝜑) → 𝜓)
21ex 449 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 52 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  sylancb  702  sylancbr  703  dedth2v  4287  dedth3v  4288  dedth4v  4289  disjprsn  4394  opidg  4572  intsng  4664  pwnss  4979  snex  5057  isso2i  5219  poinxp  5339  posn  5344  xpid11  5502  predpoirr  5869  predfrirr  5870  f1oprswap  6341  f1o2sn  6571  residpr  6572  f1mpt  6681  f1eqcocnv  6719  isopolem  6758  3xpexg  7126  sqxpexg  7128  poxp  7457  oe0  7771  oecl  7786  nnmsucr  7874  ecopover  8018  enrefg  8153  php  8309  3xpfi  8397  dffi3  8502  infxpenlem  9026  xp2cda  9194  isfin5-2  9405  fpwwe2lem5  9648  pwfseqlem4a  9675  pwfseqlem4  9676  pwfseqlem5  9677  pwfseq  9678  nqereu  9943  halfnq  9990  ltsopr  10046  1idsr  10111  00sr  10112  sqgt0sr  10119  leid  10325  msqgt0  10740  msqge0  10741  recextlem1  10849  recextlem2  10850  recex  10851  div1  10908  cju  11208  2halves  11452  msqznn  11651  xrltnr  12146  xrleid  12176  iccid  12413  m1expeven  13101  expubnd  13115  sqneg  13117  sqcl  13119  nnsqcl  13127  qsqcl  13129  subsq2  13167  bernneq  13184  faclbnd  13271  faclbnd3  13273  hashfac  13434  leiso  13435  cjmulval  14084  fallrisefac  14955  sin2t  15106  cos2t  15107  divalglem0  15318  divalglem2  15320  gcd0id  15442  lcmid  15524  lcmgcdeq  15527  lcmfsn  15550  isprm5  15621  prslem  17132  pslem  17407  dirref  17436  sgrp2nmndlem4  17616  grpsubid  17700  grp1inv  17724  cntzi  17962  symgval  17999  symgbas  18000  symgbasfi  18006  symg1bas  18016  pgrpsubgsymg  18028  symgextfve  18039  pmtrfinv  18081  psgnsn  18140  lsmidm  18277  ringadd2  18775  ipeq0  20185  matsca2  20428  matbas2  20429  matplusgcell  20441  matsubgcell  20442  mamulid  20449  mamurid  20450  mattposcl  20461  mat1dimelbas  20479  mat1dimscm  20483  mat1dimmul  20484  m1detdiag  20605  mdetdiagid  20608  mdetunilem9  20628  pmatcoe1fsupp  20708  d1mat2pmat  20746  idcn  21263  hausdiag  21650  symgtgp  22106  ustref  22223  ustelimasn  22227  iducn  22288  ismet  22329  isxmet  22330  idnghm  22748  resubmet  22806  xrsxmet  22813  cphnm  23193  tchnmval  23228  ipcau2  23233  tchcphlem1  23234  tchcphlem2  23235  tchcph  23236  chordthmlem  24758  ismot  25629  hmoval  27974  htth  28084  hvsubid  28192  hvnegid  28193  hv2times  28227  hiidrcl  28261  normval  28290  issh2  28375  chjidm  28688  normcan  28744  ho2times  28987  kbpj  29124  lnop0  29134  riesz3i  29230  leoprf  29296  leopsq  29297  cvnref  29459  gtiso  29787  prsss  30271  deranglem  31455  dfpo2  31952  elfix2  32317  linedegen  32556  filnetlem2  32680  bj-ru0  33238  matunitlindflem2  33719  matunitlindf  33720  ftc1anclem3  33800  prdsbnd2  33907  reheibor  33951  ismgmOLD  33962  opidon2OLD  33966  exidreslem  33989  rngo2  34019  opideq  34433  eldmcoss2  34532  mzpf  37801  acongrep  38049  ttac  38105  mendval  38255  mendplusgfval  38257  mendmulrfval  38259  iocinico  38299  iocmbl  38300  seff  39010  sblpnf  39011  sigarid  41553  cnambpcma  41819  2leaddle2  41822  clintopval  42350
  Copyright terms: Public domain W3C validator