Theorem anidms 389

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 113	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 48	1 |- ( ph -> ps )

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  3722  pwnss  3994  posng  4510  xpid11m  4658  resiexg  4757  f1mpt  5550  f1eqcocnv  5570  isopolem  5601  poxp  5997  nnmsucr  6249  erex  6314  ecopover  6388  ecopoverg  6391  enrefg  6479  3xpfi  6639  ltsopi  6877  recexnq  6947  ltsonq  6955  ltaddnq  6964  nsmallnqq  6969  ltpopr  7152  ltposr  7307  1idsr  7312  00sr  7313  axltirr  7551  leid  7567  reapirr  8052  inelr  8059  apsqgt0  8076  apirr  8080  msqge0  8091  recextlem1  8118  recexaplem2  8119  recexap  8120  div1  8168  cju  8419  2halves  8643  msqznn  8844  xrltnr  9248  xrleid  9267  iooidg  9325  iccid  9341  m1expeven  9998  expubnd  10008  sqneg  10010  sqcl  10012  sqap0  10017  nnsqcl  10020  qsqcl  10022  subsq2  10058  bernneq  10070  faclbnd  10145  faclbnd3  10147  cjmulval  10318  sin2t  11036  cos2t  11037  gcd0id  11244  lcmid  11336  lcmgcdeq  11339  bj-snexg  11758