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  3919  pwnss  4203  posng  4747  sqxpexg  4791  xpid11  4901  resiexg  5004  f1mpt  5840  f1eqcocnv  5860  isopolem  5891  poxp  6318  nnmsucr  6574  erex  6644  ecopover  6720  ecopoverg  6723  enrefg  6855  3xpfi  7030  tapeq2  7365  netap  7366  2omotaplemap  7369  ltsopi  7433  recexnq  7503  ltsonq  7511  ltaddnq  7520  nsmallnqq  7525  ltpopr  7708  ltposr  7876  1idsr  7881  00sr  7882  axltirr  8139  leid  8156  reapirr  8650  inelr  8657  apsqgt0  8674  apirr  8678  msqge0  8689  recextlem1  8724  recexaplem2  8725  recexap  8726  div1  8776  cju  9034  2halves  9266  msqznn  9473  xrltnr  9901  xrleid  9922  iooidg  10031  iccid  10047  m1expeven  10731  expubnd  10741  sqneg  10743  sqcl  10745  sqap0  10751  nnsqcl  10754  qsqcl  10756  subsq2  10792  bernneq  10805  faclbnd  10886  faclbnd3  10888  cjmulval  11199  sin2t  12060  cos2t  12061  gcd0id  12300  lcmid  12402  lcmgcdeq  12405  intopsn  13199  mgm1  13202  sgrp1  13243  mnd1  13287  mnd1id  13288  grpsubid  13416  grp1  13438  grp1inv  13439  ringadd2  13789  ring1  13821  idcn  14684  ismet  14816  isxmet  14817  resubmet  15028  bj-snexg  15848