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  5819  f1eqcocnv  5839  isopolem  5870  poxp  6291  nnmsucr  6547  erex  6617  ecopover  6693  ecopoverg  6696  enrefg  6824  3xpfi  6995  tapeq2  7322  netap  7323  2omotaplemap  7326  ltsopi  7389  recexnq  7459  ltsonq  7467  ltaddnq  7476  nsmallnqq  7481  ltpopr  7664  ltposr  7832  1idsr  7837  00sr  7838  axltirr  8095  leid  8112  reapirr  8606  inelr  8613  apsqgt0  8630  apirr  8634  msqge0  8645  recextlem1  8680  recexaplem2  8681  recexap  8682  div1  8732  cju  8990  2halves  9222  msqznn  9428  xrltnr  9856  xrleid  9877  iooidg  9986  iccid  10002  m1expeven  10680  expubnd  10690  sqneg  10692  sqcl  10694  sqap0  10700  nnsqcl  10703  qsqcl  10705  subsq2  10741  bernneq  10754  faclbnd  10835  faclbnd3  10837  cjmulval  11055  sin2t  11916  cos2t  11917  gcd0id  12156  lcmid  12258  lcmgcdeq  12261  intopsn  13020  mgm1  13023  sgrp1  13064  mnd1  13097  mnd1id  13098  grpsubid  13226  grp1  13248  grp1inv  13249  ringadd2  13593  ring1  13625  idcn  14458  ismet  14590  isxmet  14591  resubmet  14802  bj-snexg  15568