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

Theorem anidms 392
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 114 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 49 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  sylancb  412  sylancbr  413  intsng  3773  pwnss  4051  posng  4579  sqxpexg  4623  xpid11  4730  resiexg  4832  f1mpt  5638  f1eqcocnv  5658  isopolem  5689  poxp  6095  nnmsucr  6350  erex  6419  ecopover  6493  ecopoverg  6496  enrefg  6624  3xpfi  6785  ltsopi  7092  recexnq  7162  ltsonq  7170  ltaddnq  7179  nsmallnqq  7184  ltpopr  7367  ltposr  7535  1idsr  7540  00sr  7541  axltirr  7795  leid  7812  reapirr  8302  inelr  8309  apsqgt0  8326  apirr  8330  msqge0  8341  recextlem1  8372  recexaplem2  8373  recexap  8374  div1  8423  cju  8676  2halves  8900  msqznn  9102  xrltnr  9506  xrleid  9526  iooidg  9632  iccid  9648  m1expeven  10280  expubnd  10290  sqneg  10292  sqcl  10294  sqap0  10299  nnsqcl  10302  qsqcl  10304  subsq2  10340  bernneq  10352  faclbnd  10427  faclbnd3  10429  cjmulval  10600  sin2t  11355  cos2t  11356  gcd0id  11563  lcmid  11657  lcmgcdeq  11660  idcn  12276  ismet  12408  isxmet  12409  resubmet  12612  bj-snexg  12912
  Copyright terms: Public domain W3C validator