P. 6 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 501-600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	i3n2 501	Equivalence for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(a⊥ →3 b⊥ ) = ((a ∩ b) ∪ ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ))))
Theorem	ni32 502	Equivalence for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(a →3 b)⊥ = ((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))
Theorem	oi3ai3 503	Theorem for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
((a ∩ b) ∪ (a →3 b)⊥ ) = ((a ∪ b) ∩ (a⊥ →3 b⊥ ))
Theorem	i3lem1 504	Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = a⊥
Theorem	i3lem2 505	Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   a C b
Theorem	i3lem3 506	Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   ((a⊥ ∪ b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	i3lem4 507	Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   (a⊥ ∪ b) = 1
Theorem	comi31 508	Commutation theorem. (Contributed by NM, 9-Nov-1997.)
a C (a →3 b)
Theorem	com2i3 509	Commutation theorem. (Contributed by NM, 9-Nov-1997.)
a C b    &   a C c    ⇒   a C (b →3 c)
Theorem	comi32 510	Commutation theorem. (Contributed by NM, 9-Nov-1997.)
a C b    ⇒   a C (b →3 a)
Theorem	lem4 511	Lemma 4 of Kalmbach p. 240. (Contributed by NM, 5-Nov-1997.)
(a →3 (a →3 b)) = (a⊥ ∪ b)
Theorem	i0i3 512	Translation to Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(a⊥ ∪ b) = 1    ⇒   (a →3 (a →3 b)) = 1
Theorem	i3i0 513	Translation from Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(a →3 (a →3 b)) = 1    ⇒   (a⊥ ∪ b) = 1
Theorem	ska14 514	Soundness proof for KA14. (Contributed by NM, 3-Nov-1997.)
((a⊥ ∪ b) →3 (a →3 (a →3 b))) = 1
Theorem	i3le 515	L.e. to Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   a ≤ b
Theorem	bii3 516	Biconditional implies Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
((a ≡ b) →3 (a →3 b)) = 1
Theorem	binr1 517	Pavicic binary logic ax-r1 35 analog. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   (b⊥ →3 a⊥ ) = 1
Theorem	binr2 518	Pavicic binary logic ax-r2 36 analog. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   (b →3 c) = 1    ⇒   (a →3 c) = 1
Theorem	binr3 519	Pavicic binary logic ax-r3 439 analog. (Contributed by NM, 7-Nov-1997.)
(a →3 c) = 1    &   (b →3 c) = 1    ⇒   ((a ∪ b) →3 c) = 1
Theorem	i31 520	Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 1) = 1
Theorem	i3aa 521	Add antecedent. (Contributed by NM, 7-Nov-1997.)
a = 1    ⇒   (b →3 a) = 1
Theorem	i3abs1 522	Antecedent absorption. (Contributed by NM, 16-Nov-1997.)
(a →3 (a →3 (a →3 b))) = (a →3 (a →3 b))
Theorem	i3abs2 523	Antecedent absorption. (Contributed by NM, 9-Nov-1997.)
(a →3 (a →3 (a →3 b))) = 1    ⇒   (a →3 (a →3 b)) = 1
Theorem	i3abs3 524	Antecedent absorption. (Contributed by NM, 19-Nov-1997.)
((a →3 b) →3 ((a →3 b) →3 a)) = ((a →3 b) →3 a)
Theorem	i3orcom 525	Commutative law for conjunction with Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
((a ∪ b) →3 (b ∪ a)) = 1
Theorem	i3ancom 526	Commutative law for disjunction with Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
((a ∩ b) →3 (b ∩ a)) = 1
Theorem	bi3tr 527	Transitive inference. (Contributed by NM, 7-Nov-1997.)
a = b    &   (b →3 c) = 1    ⇒   (a →3 c) = 1
Theorem	i3btr 528	Transitive inference. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   b = c    ⇒   (a →3 c) = 1
Theorem	i33tr1 529	Transitive inference useful for introducing definitions. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   c = a    &   d = b    ⇒   (c →3 d) = 1
Theorem	i33tr2 530	Transitive inference useful for eliminating definitions. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   a = c    &   b = d    ⇒   (c →3 d) = 1
Theorem	i3con1 531	Contrapositive. (Contributed by NM, 7-Nov-1997.)
(a⊥ →3 b⊥ ) = 1    ⇒   (b →3 a) = 1
Theorem	i3ror 532	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   ((a ∪ c) →3 (b ∪ c)) = 1
Theorem	i3lor 533	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   ((c ∪ a) →3 (c ∪ b)) = 1
Theorem	i32or 534	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   (c →3 d) = 1    ⇒   ((a ∪ c) →3 (b ∪ d)) = 1
Theorem	i3ran 535	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   ((a ∩ c) →3 (b ∩ c)) = 1
Theorem	i3lan 536	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    ⇒   ((c ∩ a) →3 (c ∩ b)) = 1
Theorem	i32an 537	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   (c →3 d) = 1    ⇒   ((a ∩ c) →3 (b ∩ d)) = 1
Theorem	i3ri3 538	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   (b →3 a) = 1    ⇒   ((a →3 c) →3 (b →3 c)) = 1
Theorem	i3li3 539	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   (b →3 a) = 1    ⇒   ((c →3 a) →3 (c →3 b)) = 1
Theorem	i32i3 540	WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = 1    &   (b →3 a) = 1    &   (c →3 d) = 1    &   (d →3 c) = 1    ⇒   ((a →3 c) →3 (b →3 d)) = 1
Theorem	i0i3tr 541	Transitive inference. (Contributed by NM, 9-Nov-1997.)
(a →3 (a →3 b)) = 1    &   (b →3 c) = 1    ⇒   (a →3 (a →3 c)) = 1
Theorem	i3i0tr 542	Transitive inference. (Contributed by NM, 9-Nov-1997.)
(a →3 b) = 1    &   (b →3 (b →3 c)) = 1    ⇒   (a →3 (a →3 c)) = 1
Theorem	i3th1 543	Theorem for Kalmbach implication. (Contributed by NM, 16-Nov-1997.)
(a →3 (a →3 (b →3 a))) = 1
Theorem	i3th2 544	Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 (b →3 (b →3 a))) = 1
Theorem	i3th3 545	Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a⊥ →3 (a →3 (a →3 b))) = 1
Theorem	i3th4 546	Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 (b →3 b)) = 1
Theorem	i3th5 547	Theorem for Kalmbach implication. (Contributed by NM, 16-Nov-1997.)
((a →3 b) →3 (a →3 (a →3 b))) = 1
Theorem	i3th6 548	Theorem for Kalmbach implication. (Contributed by NM, 16-Nov-1997.)
((a →3 (a →3 (a →3 b))) →3 (a →3 (a →3 b))) = 1
Theorem	i3th7 549	Theorem for Kalmbach implication. (Contributed by NM, 19-Nov-1997.)
(a →3 ((a →3 b) →3 a)) = 1
Theorem	i3th8 550	Theorem for Kalmbach implication. (Contributed by NM, 19-Nov-1997.)
((a →3 b)⊥ →3 ((a →3 b) →3 a)) = 1
Theorem	i3con 551	Theorem for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
((a →3 b) →3 ((a →3 b) →3 (b⊥ →3 a⊥ ))) = 1
Theorem	i3orlem1 552	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((a ∪ c) ∩ ((a ∪ c)⊥ ∪ (b ∪ c))) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem2 553	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
(a ∩ b) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem3 554	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
c ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem4 555	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((a ∪ c)⊥ ∩ (b ∪ c)) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem5 556	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((a⊥ ∩ b⊥ ) ∩ c⊥ ) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem6 557	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((a →3 b)⊥ ∪ ((a ∪ c) →3 (b ∪ c))) = (((a ∪ b) ∩ (a⊥ →3 b⊥ )) ∪ ((a ∪ c) →3 (b ∪ c)))
Theorem	i3orlem7 558	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
(a ∩ b⊥ ) ≤ ((a →3 b)⊥ ∪ ((a ∪ c) →3 (b ∪ c)))
Theorem	i3orlem8 559	Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
(((a ∪ b) ∩ (a ∪ b⊥ )) ∩ a⊥ ) ≤ ((a →3 b)⊥ ∪ ((a ∪ c) →3 (b ∪ c)))
0.3.5  Unified disjunction
Theorem	ud1lem1 560	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a →1 b) →1 (b →1 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud1lem2 561	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (a⊥ ∩ b⊥ )) →1 a) = (a ∪ b)
Theorem	ud1lem3 562	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a →1 b) →1 (a ∪ b)) = (a ∪ b)
Theorem	ud2lem1 563	Lemma for unified disjunction. (Contributed by NM, 22-Nov-1997.)
((a →2 b) →2 (b →2 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud2lem2 564	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (a⊥ ∩ b⊥ )) →2 a) = (a ∪ b)
Theorem	ud2lem3 565	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a →2 b) →2 (a ∪ b)) = (a ∪ b)
Theorem	ud3lem1a 566	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b)⊥ ∩ (b →3 a)) = (a ∩ b⊥ )
Theorem	ud3lem1b 567	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b)⊥ ∩ (b →3 a)⊥ ) = 0
Theorem	ud3lem1c 568	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b)⊥ ∪ (b →3 a)) = (a ∪ b⊥ )
Theorem	ud3lem1d 569	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b) ∩ ((a →3 b)⊥ ∪ (b →3 a))) = ((a⊥ ∩ b⊥ ) ∪ (a ∩ (a⊥ ∪ b)))
Theorem	ud3lem1 570	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b) →3 (b →3 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud3lem2 571	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (a⊥ ∩ b⊥ )) →3 a) = (a ∪ b)
Theorem	ud3lem3a 572	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b)⊥ ∩ (a ∪ b)) = (a →3 b)⊥
Theorem	ud3lem3b 573	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b)⊥ ∩ (a ∪ b)⊥ ) = 0
Theorem	ud3lem3c 574	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b)⊥ ∪ (a ∪ b)) = (a ∪ b)
Theorem	ud3lem3d 575	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b) ∩ ((a →3 b)⊥ ∪ (a ∪ b))) = ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
Theorem	ud3lem3 576	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →3 b) →3 (a ∪ b)) = (a ∪ b)
Theorem	ud4lem1a 577	Lemma for unified disjunction. (Contributed by NM, 24-Nov-1997.)
((a →4 b) ∩ (b →4 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	ud4lem1b 578	Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
((a →4 b)⊥ ∩ (b →4 a)) = (a ∩ b⊥ )
Theorem	ud4lem1c 579	Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
((a →4 b)⊥ ∪ (b →4 a)) = (a ∪ b⊥ )
Theorem	ud4lem1d 580	Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
(((a →4 b)⊥ ∪ (b →4 a)) ∩ (b →4 a)⊥ ) = (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a)
Theorem	ud4lem1 581	Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
((a →4 b) →4 (b →4 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud4lem2 582	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (a⊥ ∩ b⊥ )) →4 a) = (a ∪ b)
Theorem	ud4lem3a 583	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a →4 b)⊥ ∩ (a ∪ b)) = (a →4 b)⊥
Theorem	ud4lem3b 584	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a →4 b)⊥ ∪ (a ∪ b)) = (a ∪ b)
Theorem	ud4lem3 585	Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a →4 b) →4 (a ∪ b)) = (a ∪ b)
Theorem	ud5lem1a 586	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →5 b) ∩ (b →5 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	ud5lem1b 587	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →5 b)⊥ ∩ (b →5 a)) = (a ∩ b⊥ )
Theorem	ud5lem1c 588	Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a →5 b)⊥ ∩ (b →5 a)⊥ ) = (((a ∪ b) ∩ (a ∪ b⊥ )) ∩ ((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )))
Theorem	ud5lem1 589	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →5 b) →5 (b →5 a)) = (a ∪ b⊥ )
Theorem	ud5lem2 590	Lemma for unified disjunction. (Contributed by NM, 10-Apr-2012.)
((a ∪ b⊥ ) →5 a) = (a ∪ (a⊥ ∩ b))
Theorem	ud5lem3a 591	Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a →5 b) ∩ (a ∪ (a⊥ ∩ b))) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	ud5lem3b 592	Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a →5 b)⊥ ∩ (a ∪ (a⊥ ∩ b))) = (a ∩ (a⊥ ∪ b⊥ ))
Theorem	ud5lem3c 593	Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a →5 b)⊥ ∩ (a ∪ (a⊥ ∩ b))⊥ ) = (((a ∪ b) ∩ (a ∪ b⊥ )) ∩ a⊥ )
Theorem	ud5lem3 594	Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a →5 b) →5 (a ∪ (a⊥ ∩ b))) = (a ∪ b)
Theorem	ud1 595	Unified disjunction for Sasaki implication. (Contributed by NM, 23-Nov-1997.)
(a ∪ b) = ((a →1 b) →1 (((a →1 b) →1 (b →1 a)) →1 a))
Theorem	ud2 596	Unified disjunction for Dishkant implication. (Contributed by NM, 23-Nov-1997.)
(a ∪ b) = ((a →2 b) →2 (((a →2 b) →2 (b →2 a)) →2 a))
Theorem	ud3 597	Unified disjunction for Kalmbach implication. (Contributed by NM, 23-Nov-1997.)
(a ∪ b) = ((a →3 b) →3 (((a →3 b) →3 (b →3 a)) →3 a))
Theorem	ud4 598	Unified disjunction for non-tollens implication. (Contributed by NM, 23-Nov-1997.)
(a ∪ b) = ((a →4 b) →4 (((a →4 b) →4 (b →4 a)) →4 a))
Theorem	ud5 599	Unified disjunction for relevance implication. (Contributed by NM, 23-Nov-1997.)
(a ∪ b) = ((a →5 b) →5 (((a →5 b) →5 (b →5 a)) →5 a))
0.3.6  Lemmas for unified implication study
Theorem	u1lemaa 600	Lemma for Sasaki implication study. Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by NM, 14-Dec-1997.)
((a →1 b) ∩ a) = (a ∩ b)