Theorem anidms 332

Description: Inference from idempotent law for conjunction.

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  sylancb 362  sylancbr 363  anabss1 381  anabss3 382  anabss5 384  so 2152  oe0 3130  oesuc 3134  oecl 3140  nnmsucr 3182  erref 3212  ecopoprdm 3245  php 3409  r1pwcl 3530  cdainf 3731  recmulpq 3864  ltapq 3870  halfpq 3876  ltsopr 3930  1idsr 4001  00sr 4002  sqgt0sr 4009  ssgt0sr 4011  subidt 4159  leidt 4293  sqgt0 4343  le2sqt 4420  nnunb 4520  znnsubt 4595  sqznn 4600  uzind 4603  sqclt 4684  nnesq 4720  sqr0 4730  sqrlem4 4734  sqrlem5 4735  sqrlem6 4736  sqrlem12 4742  sqrlem21 4751  sqrlem22 4752  sqrlem24 4754  sqrgt0i 4755  sqrlem26 4756  sqr11 4761  sqrsq 4764  infxpidmlem7 4939  infxpidmlem10 4942  infxpidmlem12 4944  infdif 4948  hvsubidt 5005  hvnegidt 5006  hiidrclt 5053  normvalt 5075  chjidmt 5436  cvnreft 5723

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org