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  3893  pwnss  4177  posng  4716  sqxpexg  4760  xpid11  4868  resiexg  4970  f1mpt  5793  f1eqcocnv  5813  isopolem  5844  poxp  6257  nnmsucr  6513  erex  6583  ecopover  6659  ecopoverg  6662  enrefg  6790  3xpfi  6959  tapeq2  7282  netap  7283  2omotaplemap  7286  ltsopi  7349  recexnq  7419  ltsonq  7427  ltaddnq  7436  nsmallnqq  7441  ltpopr  7624  ltposr  7792  1idsr  7797  00sr  7798  axltirr  8054  leid  8071  reapirr  8564  inelr  8571  apsqgt0  8588  apirr  8592  msqge0  8603  recextlem1  8638  recexaplem2  8639  recexap  8640  div1  8690  cju  8948  2halves  9178  msqznn  9383  xrltnr  9809  xrleid  9830  iooidg  9939  iccid  9955  m1expeven  10598  expubnd  10608  sqneg  10610  sqcl  10612  sqap0  10618  nnsqcl  10621  qsqcl  10623  subsq2  10659  bernneq  10672  faclbnd  10753  faclbnd3  10755  cjmulval  10929  sin2t  11789  cos2t  11790  gcd0id  12012  lcmid  12112  lcmgcdeq  12115  intopsn  12843  mgm1  12846  sgrp1  12874  mnd1  12907  mnd1id  12908  grpsubid  13028  grp1  13050  grp1inv  13051  ringadd2  13381  ring1  13411  idcn  14172  ismet  14304  isxmet  14305  resubmet  14508  bj-snexg  15125