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

Theorem anidms 394
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 114 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 49 1 (𝜑𝜓)
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  414  sylancbr  415  intsng  3775  pwnss  4053  posng  4581  sqxpexg  4625  xpid11  4732  resiexg  4834  f1mpt  5640  f1eqcocnv  5660  isopolem  5691  poxp  6097  nnmsucr  6352  erex  6421  ecopover  6495  ecopoverg  6498  enrefg  6626  3xpfi  6787  ltsopi  7096  recexnq  7166  ltsonq  7174  ltaddnq  7183  nsmallnqq  7188  ltpopr  7371  ltposr  7539  1idsr  7544  00sr  7545  axltirr  7799  leid  7816  reapirr  8307  inelr  8314  apsqgt0  8331  apirr  8335  msqge0  8346  recextlem1  8380  recexaplem2  8381  recexap  8382  div1  8431  cju  8687  2halves  8917  msqznn  9119  xrltnr  9534  xrleid  9554  iooidg  9660  iccid  9676  m1expeven  10308  expubnd  10318  sqneg  10320  sqcl  10322  sqap0  10327  nnsqcl  10330  qsqcl  10332  subsq2  10368  bernneq  10380  faclbnd  10455  faclbnd3  10457  cjmulval  10628  sin2t  11383  cos2t  11384  gcd0id  11594  lcmid  11688  lcmgcdeq  11691  idcn  12308  ismet  12440  isxmet  12441  resubmet  12644  bj-snexg  13037
  Copyright terms: Public domain W3C validator