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  3878  pwnss  4159  posng  4698  sqxpexg  4742  xpid11  4850  resiexg  4952  f1mpt  5771  f1eqcocnv  5791  isopolem  5822  poxp  6232  nnmsucr  6488  erex  6558  ecopover  6632  ecopoverg  6635  enrefg  6763  3xpfi  6929  tapeq2  7251  netap  7252  2omotaplemap  7255  ltsopi  7318  recexnq  7388  ltsonq  7396  ltaddnq  7405  nsmallnqq  7410  ltpopr  7593  ltposr  7761  1idsr  7766  00sr  7767  axltirr  8023  leid  8040  reapirr  8533  inelr  8540  apsqgt0  8557  apirr  8561  msqge0  8572  recextlem1  8607  recexaplem2  8608  recexap  8609  div1  8659  cju  8917  2halves  9147  msqznn  9352  xrltnr  9778  xrleid  9799  iooidg  9908  iccid  9924  m1expeven  10566  expubnd  10576  sqneg  10578  sqcl  10580  sqap0  10586  nnsqcl  10589  qsqcl  10591  subsq2  10627  bernneq  10640  faclbnd  10720  faclbnd3  10722  cjmulval  10896  sin2t  11756  cos2t  11757  gcd0id  11979  lcmid  12079  lcmgcdeq  12082  intopsn  12785  mgm1  12788  sgrp1  12815  mnd1  12846  mnd1id  12847  grpsubid  12953  grp1  12975  grp1inv  12976  ringadd2  13208  ring1  13234  idcn  13682  ismet  13814  isxmet  13815  resubmet  14018  bj-snexg  14634