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  6569  ltposr  6691  1idsr  6696  00sr  6697  axltirr  6883  leid  6899  reapirr  7361  inelr  7368  apsqgt0  7385  apirr  7389  msqge0  7400  recextlem1  7414  recexaplem2  7415  recexap  7416  div1  7462  cju  7694  2halves  7931  msqznn  8114  xrltnr  8471  xrleid  8490  iooidg  8548  iccid  8564  expubnd  8965  sqneg  8967  sqcl  8969  nnsqcl  8976  qsqcl  8978  subsq2  9012  bernneq  9022  cjmulval  9116  bj-snexg  9367
  Copyright terms: Public domain W3C validator