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  3905  pwnss  4189  posng  4732  sqxpexg  4776  xpid11  4886  resiexg  4988  f1mpt  5815  f1eqcocnv  5835  isopolem  5866  poxp  6287  nnmsucr  6543  erex  6613  ecopover  6689  ecopoverg  6692  enrefg  6820  3xpfi  6989  tapeq2  7315  netap  7316  2omotaplemap  7319  ltsopi  7382  recexnq  7452  ltsonq  7460  ltaddnq  7469  nsmallnqq  7474  ltpopr  7657  ltposr  7825  1idsr  7830  00sr  7831  axltirr  8088  leid  8105  reapirr  8598  inelr  8605  apsqgt0  8622  apirr  8626  msqge0  8637  recextlem1  8672  recexaplem2  8673  recexap  8674  div1  8724  cju  8982  2halves  9214  msqznn  9420  xrltnr  9848  xrleid  9869  iooidg  9978  iccid  9994  m1expeven  10660  expubnd  10670  sqneg  10672  sqcl  10674  sqap0  10680  nnsqcl  10683  qsqcl  10685  subsq2  10721  bernneq  10734  faclbnd  10815  faclbnd3  10817  cjmulval  11035  sin2t  11895  cos2t  11896  gcd0id  12119  lcmid  12221  lcmgcdeq  12224  intopsn  12953  mgm1  12956  sgrp1  12997  mnd1  13030  mnd1id  13031  grpsubid  13159  grp1  13181  grp1inv  13182  ringadd2  13526  ring1  13558  idcn  14391  ismet  14523  isxmet  14524  resubmet  14735  bj-snexg  15474