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

Theorem anidms 395
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  415  sylancbr  416  intsng  3812  pwnss  4090  posng  4618  sqxpexg  4662  xpid11  4769  resiexg  4871  f1mpt  5679  f1eqcocnv  5699  isopolem  5730  poxp  6136  nnmsucr  6391  erex  6460  ecopover  6534  ecopoverg  6537  enrefg  6665  3xpfi  6826  ltsopi  7151  recexnq  7221  ltsonq  7229  ltaddnq  7238  nsmallnqq  7243  ltpopr  7426  ltposr  7594  1idsr  7599  00sr  7600  axltirr  7854  leid  7871  reapirr  8362  inelr  8369  apsqgt0  8386  apirr  8390  msqge0  8401  recextlem1  8435  recexaplem2  8436  recexap  8437  div1  8486  cju  8742  2halves  8972  msqznn  9174  xrltnr  9595  xrleid  9615  iooidg  9721  iccid  9737  m1expeven  10370  expubnd  10380  sqneg  10382  sqcl  10384  sqap0  10389  nnsqcl  10392  qsqcl  10394  subsq2  10430  bernneq  10442  faclbnd  10518  faclbnd3  10520  cjmulval  10691  sin2t  11490  cos2t  11491  gcd0id  11701  lcmid  11795  lcmgcdeq  11798  idcn  12418  ismet  12550  isxmet  12551  resubmet  12754  bj-snexg  13279
  Copyright terms: Public domain W3C validator