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  3957  pwnss  4243  posng  4791  sqxpexg  4835  xpid11  4947  resiexg  5050  f1mpt  5901  f1eqcocnv  5921  isopolem  5952  poxp  6384  nnmsucr  6642  erex  6712  ecopover  6788  ecopoverg  6791  enrefg  6923  3xpfi  7106  tapeq2  7450  netap  7451  2omotaplemap  7454  ltsopi  7518  recexnq  7588  ltsonq  7596  ltaddnq  7605  nsmallnqq  7610  ltpopr  7793  ltposr  7961  1idsr  7966  00sr  7967  axltirr  8224  leid  8241  reapirr  8735  inelr  8742  apsqgt0  8759  apirr  8763  msqge0  8774  recextlem1  8809  recexaplem2  8810  recexap  8811  div1  8861  cju  9119  2halves  9351  msqznn  9558  xrltnr  9987  xrleid  10008  iooidg  10117  iccid  10133  m1expeven  10820  expubnd  10830  sqneg  10832  sqcl  10834  sqap0  10840  nnsqcl  10843  qsqcl  10845  subsq2  10881  bernneq  10894  faclbnd  10975  faclbnd3  10977  cjmulval  11415  sin2t  12276  cos2t  12277  gcd0id  12516  lcmid  12618  lcmgcdeq  12621  intopsn  13416  mgm1  13419  sgrp1  13460  mnd1  13504  mnd1id  13505  grpsubid  13633  grp1  13655  grp1inv  13656  ringadd2  14006  ring1  14038  idcn  14902  ismet  15034  isxmet  15035  resubmet  15246  bj-snexg  16358