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  3988  pwnss  4277  posng  4827  sqxpexg  4873  xpid11  4985  resiexg  5088  f1mpt  5950  f1eqcocnv  5970  isopolem  6001  poxp  6441  nnmsucr  6734  erex  6804  ecopover  6880  ecopoverg  6883  enrefg  7016  3xpfi  7207  tapeq2  7583  netap  7584  2omotaplemap  7587  ltsopi  7651  recexnq  7721  ltsonq  7729  ltaddnq  7738  nsmallnqq  7743  ltpopr  7926  ltposr  8094  1idsr  8099  00sr  8100  axltirr  8356  leid  8373  reapirr  8868  inelr  8875  apsqgt0  8892  apirr  8896  msqge0  8907  recextlem1  8942  recexaplem2  8943  recexap  8944  div1  8994  cju  9252  2halves  9484  msqznn  9696  xrltnr  10131  xrleid  10152  iooidg  10261  iccid  10277  m1expeven  10972  expubnd  10982  sqneg  10984  sqcl  10986  sqap0  10992  nnsqcl  10995  qsqcl  10997  subsq2  11033  bernneq  11047  faclbnd  11128  faclbnd3  11130  cjmulval  11598  sin2t  12460  cos2t  12461  gcd0id  12700  lcmid  12802  lcmgcdeq  12805  intopsn  13630  mgm1  13633  sgrp1  13674  mnd1  13710  mnd1id  13711  grpsubid  13839  grp1  13861  grp1inv  13862  ringadd2  14270  ring1  14302  idcn  15203  ismet  15335  isxmet  15336  resubmet  15547  bj-snexg  16808