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  3957  pwnss  4243  posng  4791  sqxpexg  4835  xpid11  4947  resiexg  5050  f1mpt  5895  f1eqcocnv  5915  isopolem  5946  poxp  6378  nnmsucr  6634  erex  6704  ecopover  6780  ecopoverg  6783  enrefg  6915  3xpfi  7095  tapeq2  7439  netap  7440  2omotaplemap  7443  ltsopi  7507  recexnq  7577  ltsonq  7585  ltaddnq  7594  nsmallnqq  7599  ltpopr  7782  ltposr  7950  1idsr  7955  00sr  7956  axltirr  8213  leid  8230  reapirr  8724  inelr  8731  apsqgt0  8748  apirr  8752  msqge0  8763  recextlem1  8798  recexaplem2  8799  recexap  8800  div1  8850  cju  9108  2halves  9340  msqznn  9547  xrltnr  9975  xrleid  9996  iooidg  10105  iccid  10121  m1expeven  10808  expubnd  10818  sqneg  10820  sqcl  10822  sqap0  10828  nnsqcl  10831  qsqcl  10833  subsq2  10869  bernneq  10882  faclbnd  10963  faclbnd3  10965  cjmulval  11399  sin2t  12260  cos2t  12261  gcd0id  12500  lcmid  12602  lcmgcdeq  12605  intopsn  13400  mgm1  13403  sgrp1  13444  mnd1  13488  mnd1id  13489  grpsubid  13617  grp1  13639  grp1inv  13640  ringadd2  13990  ring1  14022  idcn  14886  ismet  15018  isxmet  15019  resubmet  15230  bj-snexg  16275