Theorem anidms 395

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  415  sylancbr  416  intsng  3813  pwnss  4091  posng  4619  sqxpexg  4663  xpid11  4770  resiexg  4872  f1mpt  5680  f1eqcocnv  5700  isopolem  5731  poxp  6137  nnmsucr  6392  erex  6461  ecopover  6535  ecopoverg  6538  enrefg  6666  3xpfi  6827  ltsopi  7152  recexnq  7222  ltsonq  7230  ltaddnq  7239  nsmallnqq  7244  ltpopr  7427  ltposr  7595  1idsr  7600  00sr  7601  axltirr  7855  leid  7872  reapirr  8363  inelr  8370  apsqgt0  8387  apirr  8391  msqge0  8402  recextlem1  8436  recexaplem2  8437  recexap  8438  div1  8487  cju  8743  2halves  8973  msqznn  9175  xrltnr  9596  xrleid  9616  iooidg  9722  iccid  9738  m1expeven  10371  expubnd  10381  sqneg  10383  sqcl  10385  sqap0  10390  nnsqcl  10393  qsqcl  10395  subsq2  10431  bernneq  10443  faclbnd  10519  faclbnd3  10521  cjmulval  10692  sin2t  11492  cos2t  11493  gcd0id  11703  lcmid  11797  lcmgcdeq  11800  idcn  12420  ismet  12552  isxmet  12553  resubmet  12756  bj-snexg  13281