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  3904  pwnss  4188  posng  4731  sqxpexg  4775  xpid11  4885  resiexg  4987  f1mpt  5814  f1eqcocnv  5834  isopolem  5865  poxp  6285  nnmsucr  6541  erex  6611  ecopover  6687  ecopoverg  6690  enrefg  6818  3xpfi  6987  tapeq2  7313  netap  7314  2omotaplemap  7317  ltsopi  7380  recexnq  7450  ltsonq  7458  ltaddnq  7467  nsmallnqq  7472  ltpopr  7655  ltposr  7823  1idsr  7828  00sr  7829  axltirr  8086  leid  8103  reapirr  8596  inelr  8603  apsqgt0  8620  apirr  8624  msqge0  8635  recextlem1  8670  recexaplem2  8671  recexap  8672  div1  8722  cju  8980  2halves  9211  msqznn  9417  xrltnr  9845  xrleid  9866  iooidg  9975  iccid  9991  m1expeven  10657  expubnd  10667  sqneg  10669  sqcl  10671  sqap0  10677  nnsqcl  10680  qsqcl  10682  subsq2  10718  bernneq  10731  faclbnd  10812  faclbnd3  10814  cjmulval  11032  sin2t  11892  cos2t  11893  gcd0id  12116  lcmid  12218  lcmgcdeq  12221  intopsn  12950  mgm1  12953  sgrp1  12994  mnd1  13027  mnd1id  13028  grpsubid  13156  grp1  13178  grp1inv  13179  ringadd2  13523  ring1  13555  idcn  14380  ismet  14512  isxmet  14513  resubmet  14716  bj-snexg  15404