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

Theorem anidms 397
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 115 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 49 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  sylancb  418  sylancbr  419  intsng  3876  pwnss  4156  posng  4695  sqxpexg  4739  xpid11  4846  resiexg  4948  f1mpt  5766  f1eqcocnv  5786  isopolem  5817  poxp  6227  nnmsucr  6483  erex  6553  ecopover  6627  ecopoverg  6630  enrefg  6758  3xpfi  6924  netap  7243  2omotaplemap  7246  ltsopi  7307  recexnq  7377  ltsonq  7385  ltaddnq  7394  nsmallnqq  7399  ltpopr  7582  ltposr  7750  1idsr  7755  00sr  7756  axltirr  8011  leid  8028  reapirr  8521  inelr  8528  apsqgt0  8545  apirr  8549  msqge0  8560  recextlem1  8594  recexaplem2  8595  recexap  8596  div1  8646  cju  8904  2halves  9134  msqznn  9339  xrltnr  9763  xrleid  9784  iooidg  9893  iccid  9909  m1expeven  10550  expubnd  10560  sqneg  10562  sqcl  10564  sqap0  10569  nnsqcl  10572  qsqcl  10574  subsq2  10610  bernneq  10623  faclbnd  10702  faclbnd3  10704  cjmulval  10878  sin2t  11738  cos2t  11739  gcd0id  11960  lcmid  12060  lcmgcdeq  12063  intopsn  12675  mgm1  12678  sgrp1  12705  mnd1  12734  mnd1id  12735  grpsubid  12840  grp1  12862  grp1inv  12863  ringadd2  13033  ring1  13059  idcn  13376  ismet  13508  isxmet  13509  resubmet  13712  bj-snexg  14317
  Copyright terms: Public domain W3C validator