Axiom ax-newstateeq 1045

Description: New equation that holds in Hilbert space, discovered by Pavicic and Megill (unpublished).

Assertion

Ref	Expression
ax-newstateeq	(((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a))) ≤ (c →1 a)

Detailed syntax breakdown of Axiom ax-newstateeq

Step	Hyp	Ref	Expression
1		wva	. . . . 5 term  a
2		wvb	. . . . 5 term  b
3	1, 2	wi1 12	. . . 4 term  (a →1 b)
4		wvc	. . . . 5 term  c
5	4, 2	wi1 12	. . . 4 term  (c →1 b)
6	3, 5	wi1 12	. . 3 term  ((a →1 b) →1 (c →1 b))
7	1, 4	wi1 12	. . . 4 term  (a →1 c)
8	2, 1	wi1 12	. . . 4 term  (b →1 a)
9	7, 8	wa 7	. . 3 term  ((a →1 c) ∩ (b →1 a))
10	6, 9	wa 7	. 2 term  (((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a)))
11	4, 1	wi1 12	. 2 term  (c →1 a)
12	10, 11	wle 2	1 wff  (((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a))) ≤ (c →1 a)

This axiom is referenced by: (None)