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  3962  pwnss  4249  posng  4798  sqxpexg  4843  xpid11  4955  resiexg  5058  f1mpt  5912  f1eqcocnv  5932  isopolem  5963  poxp  6397  nnmsucr  6656  erex  6726  ecopover  6802  ecopoverg  6805  enrefg  6937  3xpfi  7126  tapeq2  7472  netap  7473  2omotaplemap  7476  ltsopi  7540  recexnq  7610  ltsonq  7618  ltaddnq  7627  nsmallnqq  7632  ltpopr  7815  ltposr  7983  1idsr  7988  00sr  7989  axltirr  8246  leid  8263  reapirr  8757  inelr  8764  apsqgt0  8781  apirr  8785  msqge0  8796  recextlem1  8831  recexaplem2  8832  recexap  8833  div1  8883  cju  9141  2halves  9373  msqznn  9580  xrltnr  10014  xrleid  10035  iooidg  10144  iccid  10160  m1expeven  10849  expubnd  10859  sqneg  10861  sqcl  10863  sqap0  10869  nnsqcl  10872  qsqcl  10874  subsq2  10910  bernneq  10923  faclbnd  11004  faclbnd3  11006  cjmulval  11466  sin2t  12328  cos2t  12329  gcd0id  12568  lcmid  12670  lcmgcdeq  12673  intopsn  13468  mgm1  13471  sgrp1  13512  mnd1  13556  mnd1id  13557  grpsubid  13685  grp1  13707  grp1inv  13708  ringadd2  14059  ring1  14091  idcn  14955  ismet  15087  isxmet  15088  resubmet  15299  bj-snexg  16558