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  3909  pwnss  4193  posng  4736  sqxpexg  4780  xpid11  4890  resiexg  4992  f1mpt  5821  f1eqcocnv  5841  isopolem  5872  poxp  6299  nnmsucr  6555  erex  6625  ecopover  6701  ecopoverg  6704  enrefg  6832  3xpfi  7003  tapeq2  7336  netap  7337  2omotaplemap  7340  ltsopi  7404  recexnq  7474  ltsonq  7482  ltaddnq  7491  nsmallnqq  7496  ltpopr  7679  ltposr  7847  1idsr  7852  00sr  7853  axltirr  8110  leid  8127  reapirr  8621  inelr  8628  apsqgt0  8645  apirr  8649  msqge0  8660  recextlem1  8695  recexaplem2  8696  recexap  8697  div1  8747  cju  9005  2halves  9237  msqznn  9443  xrltnr  9871  xrleid  9892  iooidg  10001  iccid  10017  m1expeven  10695  expubnd  10705  sqneg  10707  sqcl  10709  sqap0  10715  nnsqcl  10718  qsqcl  10720  subsq2  10756  bernneq  10769  faclbnd  10850  faclbnd3  10852  cjmulval  11070  sin2t  11931  cos2t  11932  gcd0id  12171  lcmid  12273  lcmgcdeq  12276  intopsn  13069  mgm1  13072  sgrp1  13113  mnd1  13157  mnd1id  13158  grpsubid  13286  grp1  13308  grp1inv  13309  ringadd2  13659  ring1  13691  idcn  14532  ismet  14664  isxmet  14665  resubmet  14876  bj-snexg  15642