Theorem anidms 397

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  sylancb  418  sylancbr  419  intsng  3967  pwnss  4255  posng  4804  sqxpexg  4849  xpid11  4961  resiexg  5064  f1mpt  5922  f1eqcocnv  5942  isopolem  5973  poxp  6406  nnmsucr  6699  erex  6769  ecopover  6845  ecopoverg  6848  enrefg  6980  3xpfi  7169  tapeq2  7532  netap  7533  2omotaplemap  7536  ltsopi  7600  recexnq  7670  ltsonq  7678  ltaddnq  7687  nsmallnqq  7692  ltpopr  7875  ltposr  8043  1idsr  8048  00sr  8049  axltirr  8305  leid  8322  reapirr  8816  inelr  8823  apsqgt0  8840  apirr  8844  msqge0  8855  recextlem1  8890  recexaplem2  8891  recexap  8892  div1  8942  cju  9200  2halves  9432  msqznn  9641  xrltnr  10075  xrleid  10096  iooidg  10205  iccid  10221  m1expeven  10911  expubnd  10921  sqneg  10923  sqcl  10925  sqap0  10931  nnsqcl  10934  qsqcl  10936  subsq2  10972  bernneq  10985  faclbnd  11066  faclbnd3  11068  cjmulval  11528  sin2t  12390  cos2t  12391  gcd0id  12630  lcmid  12732  lcmgcdeq  12735  intopsn  13530  mgm1  13533  sgrp1  13574  mnd1  13618  mnd1id  13619  grpsubid  13747  grp1  13769  grp1inv  13770  ringadd2  14121  ring1  14153  idcn  15023  ismet  15155  isxmet  15156  resubmet  15367  bj-snexg  16628