ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anidms Unicode version

Theorem anidms 397
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 115 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 49 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  sylancb  418  sylancbr  419  intsng  3876  pwnss  4156  posng  4694  sqxpexg  4738  xpid11  4845  resiexg  4947  f1mpt  5765  f1eqcocnv  5785  isopolem  5816  poxp  6226  nnmsucr  6482  erex  6552  ecopover  6626  ecopoverg  6629  enrefg  6757  3xpfi  6923  ltsopi  7297  recexnq  7367  ltsonq  7375  ltaddnq  7384  nsmallnqq  7389  ltpopr  7572  ltposr  7740  1idsr  7745  00sr  7746  axltirr  8001  leid  8018  reapirr  8511  inelr  8518  apsqgt0  8535  apirr  8539  msqge0  8550  recextlem1  8584  recexaplem2  8585  recexap  8586  div1  8636  cju  8894  2halves  9124  msqznn  9329  xrltnr  9753  xrleid  9774  iooidg  9883  iccid  9899  m1expeven  10540  expubnd  10550  sqneg  10552  sqcl  10554  sqap0  10559  nnsqcl  10562  qsqcl  10564  subsq2  10600  bernneq  10613  faclbnd  10692  faclbnd3  10694  cjmulval  10868  sin2t  11728  cos2t  11729  gcd0id  11950  lcmid  12050  lcmgcdeq  12053  intopsn  12665  mgm1  12668  sgrp1  12695  mnd1  12724  mnd1id  12725  grpsubid  12830  grp1  12852  grp1inv  12853  ringadd2  13023  ring1  13049  idcn  13345  ismet  13477  isxmet  13478  resubmet  13681  bj-snexg  14286
  Copyright terms: Public domain W3C validator