Theorem 3anidm23 881

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 830	. . 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 773

This theorem is referenced by:  so 2855  pncant 5369  npcant 5371  subeq0t 5375  halfaddsubt 5988  avglet 5991  efsubt 7313  bastgt 7564  met0 7754  ioo2bl 7851  grpidinvlem1 7982  grpdivid 8024  nvmid 8225  ipid 8297  5oalem1 9516  3oalem2 9525  unopf1ot 9756  unopnormt 9757  hmopret 9763  cayleylem2 10317

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 775

Copyright terms: Public domain