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

Theorem anidms 383
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 112 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 47 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  sylancb  403  sylancbr  404  intsng  3677  pwnss  3940  posng  4440  xpid11m  4585  resiexg  4681  f1mpt  5438  f1eqcocnv  5459  isopolem  5489  poxp  5881  nnmsucr  6098  erex  6161  ecopover  6235  ecopoverg  6238  enrefg  6275  ltsopi  6476  recexnq  6546  ltsonq  6554  ltaddnq  6563  nsmallnqq  6568  ltpopr  6751  ltposr  6906  1idsr  6911  00sr  6912  axltirr  7145  leid  7161  reapirr  7642  inelr  7649  apsqgt0  7666  apirr  7670  msqge0  7681  recextlem1  7706  recexaplem2  7707  recexap  7708  div1  7754  cju  7989  2halves  8211  msqznn  8397  xrltnr  8802  xrleid  8821  iooidg  8879  iccid  8895  m1expeven  9467  expubnd  9477  sqneg  9479  sqcl  9481  sqap0  9486  nnsqcl  9489  qsqcl  9491  subsq2  9526  bernneq  9537  faclbnd  9609  faclbnd3  9611  cjmulval  9716  bj-snexg  10419
  Copyright terms: Public domain W3C validator