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

Theorem anidms 377
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 108 . 2 (φ → (φψ))
32pm2.43i 43 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  sylancb  395  sylancbr  396  intsng  3640  pwnss  3903  posng  4355  xpid11m  4500  resiexg  4596  f1mpt  5353  f1eqcocnv  5374  isopolem  5404  poxp  5794  nnmsucr  6006  erex  6066  ecopover  6140  ecopoverg  6143  enrefg  6180  ltsopi  6304  recexnq  6374  ltsonq  6382  ltaddnq  6390  nsmallnqq  6395  ltpopr  6568  ltposr  6671  1idsr  6676  00sr  6677  axltirr  6863  leid  6879  reapirr  7341  inelr  7348  apsqgt0  7365  apirr  7369  msqge0  7380  recextlem1  7394  recexaplem2  7395  recexap  7396  div1  7442  cju  7674  2halves  7911  msqznn  8094  xrltnr  8451  xrleid  8470  iooidg  8528  iccid  8544  expubnd  8945  sqneg  8947  sqcl  8949  nnsqcl  8956  qsqcl  8958  subsq2  8992  bernneq  9002  cjmulval  9096  bj-snexg  9343
  Copyright terms: Public domain W3C validator