Theorem 3anidm23 884

Description: Inference from idempotent law for conjunction.

Hypothesis

Ref	Expression
3anidm23.1	|- ((ph /\ ps /\ ps) -> ch)

Assertion

Ref	Expression
3anidm23	|- ((ph /\ ps) -> ch)

Proof of Theorem 3anidm23

Step	Hyp	Ref	Expression
1		3anidm23.1	. . . 4 |- ((ph /\ ps /\ ps) -> ch)
2	1	3exp 832	. . 3 |- (ph -> (ps -> (ps -> ch)))
3	2	pm2.43d 65	. 2 |- (ph -> (ps -> ch))
4	3	imp 350	1 |- ((ph /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  so 2864  pncant 5397  npcant 5399  subeq0t 5403  halfaddsubt 6041  avglet 6044  efsubt 7371  bastgt 7622  met0 7815  ioo2bl 7912  grpidinvlem1 8048  grpdivid 8089  nvmid 8285  ipid 8363  5oalem1 9599  3oalem2 9608  unopf1ot 9840  unopnormt 9841  hmopret 9847  cayleylem2 10410  nnssi2 10419  nndivlub 10422

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain