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

Theorem anidms 389
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 113 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 48 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  sylancb  409  sylancbr  410  intsng  3707  pwnss  3971  posng  4480  xpid11m  4628  resiexg  4726  f1mpt  5513  f1eqcocnv  5533  isopolem  5564  poxp  5956  nnmsucr  6205  erex  6270  ecopover  6344  ecopoverg  6347  enrefg  6435  3xpfi  6594  ltsopi  6826  recexnq  6896  ltsonq  6904  ltaddnq  6913  nsmallnqq  6918  ltpopr  7101  ltposr  7256  1idsr  7261  00sr  7262  axltirr  7500  leid  7516  reapirr  7998  inelr  8005  apsqgt0  8022  apirr  8026  msqge0  8037  recextlem1  8062  recexaplem2  8063  recexap  8064  div1  8112  cju  8359  2halves  8581  msqznn  8782  xrltnr  9185  xrleid  9204  iooidg  9262  iccid  9278  m1expeven  9922  expubnd  9932  sqneg  9934  sqcl  9936  sqap0  9941  nnsqcl  9944  qsqcl  9946  subsq2  9981  bernneq  9992  faclbnd  10067  faclbnd3  10069  cjmulval  10239  gcd0id  10895  lcmid  10987  lcmgcdeq  10990  bj-snexg  11291
  Copyright terms: Public domain W3C validator