Theorem anidms 401

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  sylancb  422  sylancbr  423  intsng  4004  pwnss  4296  posng  4847  sqxpexg  4893  xpid11  5005  resiexg  5108  f1mpt  5977  f1eqcocnv  5997  isopolem  6028  poxp  6468  nnmsucr  6761  erex  6831  ecopover  6907  ecopoverg  6910  enrefg  7050  3xpfi  7241  tapeq2  7619  netap  7620  2omotaplemap  7623  ltsopi  7687  recexnq  7757  ltsonq  7765  ltaddnq  7774  nsmallnqq  7779  ltpopr  7962  ltposr  8130  1idsr  8135  00sr  8136  axltirr  8392  leid  8409  reapirr  8905  inelr  8912  apsqgt0  8929  apirr  8933  msqge0  8944  recextlem1  8979  recexaplem2  8980  recexap  8981  msqap0  8996  div1  9033  cju  9291  2halves  9534  msqznn  9746  xrltnr  10181  xrleid  10202  iooidg  10311  iccid  10327  m1expeven  11023  expubnd  11033  sqneg  11035  sqcl  11037  sqap0  11043  nnsqcl  11046  qsqcl  11048  subsq2  11084  bernneq  11098  faclbnd  11179  faclbnd3  11181  hashfac  11288  cjmulval  11653  sin2t  12516  cos2t  12517  gcd0id  12756  lcmid  12858  lcmgcdeq  12861  intopsn  13687  mgm1  13690  sgrp1  13726  mnd1  13762  mnd1id  13763  grpsubid  13889  grp1  13911  grp1inv  13912  ringadd2  14332  ring1  14364  idcn  15313  ismet  15445  isxmet  15446  resubmet  15657  bj-snexg  16938