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  4298  posng  4849  sqxpexg  4895  xpid11  5007  resiexg  5111  f1mpt  5980  f1eqcocnv  6000  isopolem  6031  poxp  6472  nnmsucr  6766  erex  6836  ecopover  6912  ecopoverg  6915  enrefg  7056  3xpfi  7247  tapeq2  7625  netap  7626  2omotaplemap  7629  ltsopi  7693  recexnq  7763  ltsonq  7771  ltaddnq  7780  nsmallnqq  7785  ltpopr  7968  ltposr  8136  1idsr  8141  00sr  8142  axltirr  8398  leid  8415  reapirr  8913  inelr  8920  apsqgt0  8937  apirr  8941  msqge0  8952  recextlem1  8987  recexaplem2  8988  recexap  8989  msqap0  9004  div1  9041  cju  9299  2halves  9545  msqznn  9756  xrltnr  10197  xrleid  10218  iooidg  10327  iccid  10343  m1expeven  11043  expubnd  11053  sqneg  11055  sqcl  11057  sqap0  11063  nnsqcl  11066  qsqcl  11068  subsq2  11104  bernneq  11118  faclbnd  11200  faclbnd3  11202  hashfac  11309  cjmulval  11674  sin2t  12540  cos2t  12541  gcd0id  12780  lcmid  12882  lcmgcdeq  12885  intopsn  13745  mgm1  13748  sgrp1  13784  mnd1  13820  mnd1id  13821  grpsubid  13947  grp1  13969  grp1inv  13970  cntzi  14161  ringadd2  14438  ring1  14470  idcn  15455  ismet  15587  isxmet  15588  resubmet  15799  bj-snexg  17160