Theorem anidms 377

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 108	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 43	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  sylancb  395  sylancbr  396  intsng  3649  pwnss  3912  posng  4412  xpid11m  4557  resiexg  4653  f1mpt  5410  f1eqcocnv  5431  isopolem  5461  poxp  5853  nnmsucr  6067  erex  6130  ecopover  6204  ecopoverg  6207  enrefg  6244  ltsopi  6418  recexnq  6488  ltsonq  6496  ltaddnq  6505  nsmallnqq  6510  ltpopr  6693  ltposr  6848  1idsr  6853  00sr  6854  axltirr  7086  leid  7102  reapirr  7568  inelr  7575  apsqgt0  7592  apirr  7596  msqge0  7607  recextlem1  7632  recexaplem2  7633  recexap  7634  div1  7680  cju  7913  2halves  8154  msqznn  8338  xrltnr  8701  xrleid  8720  iooidg  8778  iccid  8794  expubnd  9311  sqneg  9313  sqcl  9315  sqap0  9320  nnsqcl  9323  qsqcl  9325  subsq2  9359  bernneq  9369  cjmulval  9488  bj-snexg  10032