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  3879  pwnss  4160  posng  4699  sqxpexg  4743  xpid11  4851  resiexg  4953  f1mpt  5772  f1eqcocnv  5792  isopolem  5823  poxp  6233  nnmsucr  6489  erex  6559  ecopover  6633  ecopoverg  6636  enrefg  6764  3xpfi  6930  tapeq2  7252  netap  7253  2omotaplemap  7256  ltsopi  7319  recexnq  7389  ltsonq  7397  ltaddnq  7406  nsmallnqq  7411  ltpopr  7594  ltposr  7762  1idsr  7767  00sr  7768  axltirr  8024  leid  8041  reapirr  8534  inelr  8541  apsqgt0  8558  apirr  8562  msqge0  8573  recextlem1  8608  recexaplem2  8609  recexap  8610  div1  8660  cju  8918  2halves  9148  msqznn  9353  xrltnr  9779  xrleid  9800  iooidg  9909  iccid  9925  m1expeven  10567  expubnd  10577  sqneg  10579  sqcl  10581  sqap0  10587  nnsqcl  10590  qsqcl  10592  subsq2  10628  bernneq  10641  faclbnd  10721  faclbnd3  10723  cjmulval  10897  sin2t  11757  cos2t  11758  gcd0id  11980  lcmid  12080  lcmgcdeq  12083  intopsn  12786  mgm1  12789  sgrp1  12816  mnd1  12847  mnd1id  12848  grpsubid  12954  grp1  12976  grp1inv  12977  ringadd2  13210  ring1  13236  idcn  13715  ismet  13847  isxmet  13848  resubmet  14051  bj-snexg  14667