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  3805  pwnss  4083  posng  4611  sqxpexg  4655  xpid11  4762  resiexg  4864  f1mpt  5672  f1eqcocnv  5692  isopolem  5723  poxp  6129  nnmsucr  6384  erex  6453  ecopover  6527  ecopoverg  6530  enrefg  6658  3xpfi  6819  ltsopi  7128  recexnq  7198  ltsonq  7206  ltaddnq  7215  nsmallnqq  7220  ltpopr  7403  ltposr  7571  1idsr  7576  00sr  7577  axltirr  7831  leid  7848  reapirr  8339  inelr  8346  apsqgt0  8363  apirr  8367  msqge0  8378  recextlem1  8412  recexaplem2  8413  recexap  8414  div1  8463  cju  8719  2halves  8949  msqznn  9151  xrltnr  9566  xrleid  9586  iooidg  9692  iccid  9708  m1expeven  10340  expubnd  10350  sqneg  10352  sqcl  10354  sqap0  10359  nnsqcl  10362  qsqcl  10364  subsq2  10400  bernneq  10412  faclbnd  10487  faclbnd3  10489  cjmulval  10660  sin2t  11456  cos2t  11457  gcd0id  11667  lcmid  11761  lcmgcdeq  11764  idcn  12381  ismet  12513  isxmet  12514  resubmet  12717  bj-snexg  13110