Theorem anidms 394

Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
anidms.1	|- ( ( ph /\ ph ) -> ps )

Assertion

Ref	Expression
anidms	|- ( ph -> ps )

Proof of Theorem anidms

Step	Hyp	Ref	Expression
1		anidms.1	. . 3 |- ( ( ph /\ ph ) -> ps )
2	1	ex 114	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 49	1 |- ( ph -> ps )

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  3800  pwnss  4078  posng  4606  sqxpexg  4650  xpid11  4757  resiexg  4859  f1mpt  5665  f1eqcocnv  5685  isopolem  5716  poxp  6122  nnmsucr  6377  erex  6446  ecopover  6520  ecopoverg  6523  enrefg  6651  3xpfi  6812  ltsopi  7121  recexnq  7191  ltsonq  7199  ltaddnq  7208  nsmallnqq  7213  ltpopr  7396  ltposr  7564  1idsr  7569  00sr  7570  axltirr  7824  leid  7841  reapirr  8332  inelr  8339  apsqgt0  8356  apirr  8360  msqge0  8371  recextlem1  8405  recexaplem2  8406  recexap  8407  div1  8456  cju  8712  2halves  8942  msqznn  9144  xrltnr  9559  xrleid  9579  iooidg  9685  iccid  9701  m1expeven  10333  expubnd  10343  sqneg  10345  sqcl  10347  sqap0  10352  nnsqcl  10355  qsqcl  10357  subsq2  10393  bernneq  10405  faclbnd  10480  faclbnd3  10482  cjmulval  10653  sin2t  11445  cos2t  11446  gcd0id  11656  lcmid  11750  lcmgcdeq  11753  idcn  12370  ismet  12502  isxmet  12503  resubmet  12706  bj-snexg  13099