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 )

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  422  sylancbr  423  intsng  3999  pwnss  4291  posng  4842  sqxpexg  4888  xpid11  5000  resiexg  5103  f1mpt  5967  f1eqcocnv  5987  isopolem  6018  poxp  6458  nnmsucr  6751  erex  6821  ecopover  6897  ecopoverg  6900  enrefg  7040  3xpfi  7231  tapeq2  7609  netap  7610  2omotaplemap  7613  ltsopi  7677  recexnq  7747  ltsonq  7755  ltaddnq  7764  nsmallnqq  7769  ltpopr  7952  ltposr  8120  1idsr  8125  00sr  8126  axltirr  8382  leid  8399  reapirr  8895  inelr  8902  apsqgt0  8919  apirr  8923  msqge0  8934  recextlem1  8969  recexaplem2  8970  recexap  8971  msqap0  8986  div1  9023  cju  9281  2halves  9513  msqznn  9725  xrltnr  10160  xrleid  10181  iooidg  10290  iccid  10306  m1expeven  11001  expubnd  11011  sqneg  11013  sqcl  11015  sqap0  11021  nnsqcl  11024  qsqcl  11026  subsq2  11062  bernneq  11076  faclbnd  11157  faclbnd3  11159  hashfac  11266  cjmulval  11631  sin2t  12494  cos2t  12495  gcd0id  12734  lcmid  12836  lcmgcdeq  12839  intopsn  13664  mgm1  13667  sgrp1  13703  mnd1  13739  mnd1id  13740  grpsubid  13866  grp1  13888  grp1inv  13889  ringadd2  14305  ring1  14337  idcn  15236  ismet  15368  isxmet  15369  resubmet  15580  bj-snexg  16852