P. 7 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 601-700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	u2lemaa 601	Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a →2 b) ∩ a) = (a ∩ b)
Theorem	u3lemaa 602	Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a →3 b) ∩ a) = (a ∩ (a⊥ ∪ b))
Theorem	u4lemaa 603	Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a →4 b) ∩ a) = (a ∩ b)
Theorem	u5lemaa 604	Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a →5 b) ∩ a) = (a ∩ b)
Theorem	u1lemana 605	Lemma for Sasaki implication study. (Contributed by NM, 14-Dec-1997.)
((a →1 b) ∩ a⊥ ) = a⊥
Theorem	u2lemana 606	Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a →2 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u3lemana 607	Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a →3 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u4lemana 608	Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a →4 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u5lemana 609	Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a →5 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u1lemab 610	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) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u2lemab 611	Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a →2 b) ∩ b) = b
Theorem	u3lemab 612	Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a →3 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u4lemab 613	Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a →4 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u5lemab 614	Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a →5 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u1lemanb 615	Lemma for Sasaki implication study. (Contributed by NM, 14-Dec-1997.)
((a →1 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u2lemanb 616	Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a →2 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u3lemanb 617	Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a →3 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u4lemanb 618	Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a →4 b) ∩ b⊥ ) = ((a⊥ ∪ b) ∩ b⊥ )
Theorem	u5lemanb 619	Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a →5 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u1lemoa 620	Lemma for Sasaki implication study. (Contributed by NM, 14-Dec-1997.)
((a →1 b) ∪ a) = 1
Theorem	u2lemoa 621	Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a →2 b) ∪ a) = 1
Theorem	u3lemoa 622	Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a →3 b) ∪ a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u4lemoa 623	Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a →4 b) ∪ a) = 1
Theorem	u5lemoa 624	Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a →5 b) ∪ a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u1lemona 625	Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a →1 b) ∪ a⊥ ) = (a⊥ ∪ (a ∩ b))
Theorem	u2lemona 626	Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a →2 b) ∪ a⊥ ) = (a⊥ ∪ b)
Theorem	u3lemona 627	Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a →3 b) ∪ a⊥ ) = (a⊥ ∪ b)
Theorem	u4lemona 628	Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a →4 b) ∪ a⊥ ) = (a⊥ ∪ b)
Theorem	u5lemona 629	Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a →5 b) ∪ a⊥ ) = (a⊥ ∪ (a ∩ b))
Theorem	u1lemob 630	Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a →1 b) ∪ b) = (a⊥ ∪ b)
Theorem	u2lemob 631	Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a →2 b) ∪ b) = ((a⊥ ∩ b⊥ ) ∪ b)
Theorem	u3lemob 632	Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a →3 b) ∪ b) = (a⊥ ∪ b)
Theorem	u4lemob 633	Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a →4 b) ∪ b) = (a⊥ ∪ b)
Theorem	u5lemob 634	Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a →5 b) ∪ b) = ((a⊥ ∩ b⊥ ) ∪ b)
Theorem	u1lemonb 635	Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a →1 b) ∪ b⊥ ) = 1
Theorem	u2lemonb 636	Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a →2 b) ∪ b⊥ ) = 1
Theorem	u3lemonb 637	Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a →3 b) ∪ b⊥ ) = 1
Theorem	u4lemonb 638	Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a →4 b) ∪ b⊥ ) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ b⊥ )
Theorem	u5lemonb 639	Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a →5 b) ∪ b⊥ ) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ b⊥ )
Theorem	u1lemnaa 640	Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a →1 b)⊥ ∩ a) = (a ∩ (a⊥ ∪ b⊥ ))
Theorem	u2lemnaa 641	Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a →2 b)⊥ ∩ a) = (a ∩ b⊥ )
Theorem	u3lemnaa 642	Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a →3 b)⊥ ∩ a) = (a ∩ b⊥ )
Theorem	u4lemnaa 643	Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a →4 b)⊥ ∩ a) = (a ∩ b⊥ )
Theorem	u5lemnaa 644	Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a →5 b)⊥ ∩ a) = (a ∩ (a⊥ ∪ b⊥ ))
Theorem	u1lemnana 645	Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a →1 b)⊥ ∩ a⊥ ) = 0
Theorem	u2lemnana 646	Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a →2 b)⊥ ∩ a⊥ ) = 0
Theorem	u3lemnana 647	Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b)⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u4lemnana 648	Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a →4 b)⊥ ∩ a⊥ ) = 0
Theorem	u5lemnana 649	Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b)⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u1lemnab 650	Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a →1 b)⊥ ∩ b) = 0
Theorem	u2lemnab 651	Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a →2 b)⊥ ∩ b) = 0
Theorem	u3lemnab 652	Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b)⊥ ∩ b) = 0
Theorem	u4lemnab 653	Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b)⊥ ∩ b) = (((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ )) ∩ b)
Theorem	u5lemnab 654	Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b)⊥ ∩ b) = (((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ )) ∩ b)
Theorem	u1lemnanb 655	Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a →1 b)⊥ ∩ b⊥ ) = (a ∩ b⊥ )
Theorem	u2lemnanb 656	Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a →2 b)⊥ ∩ b⊥ ) = ((a ∪ b) ∩ b⊥ )
Theorem	u3lemnanb 657	Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b)⊥ ∩ b⊥ ) = (a ∩ b⊥ )
Theorem	u4lemnanb 658	Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b)⊥ ∩ b⊥ ) = (a ∩ b⊥ )
Theorem	u5lemnanb 659	Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b)⊥ ∩ b⊥ ) = ((a ∪ b) ∩ b⊥ )
Theorem	u1lemnoa 660	Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a →1 b)⊥ ∪ a) = a
Theorem	u2lemnoa 661	Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a →2 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u3lemnoa 662	Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u4lemnoa 663	Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u5lemnoa 664	Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u1lemnona 665	Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a →1 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u2lemnona 666	Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a →2 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u3lemnona 667	Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b)⊥ ∪ a⊥ ) = (a⊥ ∪ (a ∩ b⊥ ))
Theorem	u4lemnona 668	Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u5lemnona 669	Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u1lemnob 670	Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a →1 b)⊥ ∪ b) = (a ∪ b)
Theorem	u2lemnob 671	Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a →2 b)⊥ ∪ b) = (a ∪ b)
Theorem	u3lemnob 672	Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b)⊥ ∪ b) = (a ∪ b)
Theorem	u4lemnob 673	Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b)⊥ ∪ b) = ((a ∩ b⊥ ) ∪ b)
Theorem	u5lemnob 674	Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b)⊥ ∪ b) = (a ∪ b)
Theorem	u1lemnonb 675	Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a →1 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u2lemnonb 676	Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a →2 b)⊥ ∪ b⊥ ) = b⊥
Theorem	u3lemnonb 677	Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u4lemnonb 678	Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u5lemnonb 679	Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u1lemc1 680	Commutation theorem for Sasaki implication. (Contributed by NM, 14-Dec-1997.)
a C (a →1 b)
Theorem	u2lemc1 681	Commutation theorem for Dishkant implication. (Contributed by NM, 14-Dec-1997.)
b C (a →2 b)
Theorem	u3lemc1 682	Commutation theorem for Kalmbach implication. (Contributed by NM, 14-Dec-1997.)
a C (a →3 b)
Theorem	u4lemc1 683	Commutation theorem for non-tollens implication. (Contributed by NM, 14-Dec-1997.)
b C (a →4 b)
Theorem	u5lemc1 684	Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
a C (a →5 b)
Theorem	u5lemc1b 685	Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
b C (a →5 b)
Theorem	u1lemc2 686	Commutation theorem for Sasaki implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c    ⇒   a C (b →1 c)
Theorem	u2lemc2 687	Commutation theorem for Dishkant implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c    ⇒   a C (b →2 c)
Theorem	u3lemc2 688	Commutation theorem for Kalmbach implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c    ⇒   a C (b →3 c)
Theorem	u4lemc2 689	Commutation theorem for non-tollens implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c    ⇒   a C (b →4 c)
Theorem	u5lemc2 690	Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c    ⇒   a C (b →5 c)
Theorem	u1lemc3 691	Commutation theorem for Sasaki implication. (Contributed by NM, 14-Dec-1997.)
a C b    ⇒   a C (b →1 a)
Theorem	u2lemc3 692	Commutation theorem for Dishkant implication. (Contributed by NM, 14-Dec-1997.)
a C b    ⇒   a C (b →2 a)
Theorem	u3lemc3 693	Commutation theorem for Kalmbach implication. (Contributed by NM, 14-Dec-1997.)
a C b    ⇒   a C (b →3 a)
Theorem	u4lemc3 694	Commutation theorem for non-tollens implication. (Contributed by NM, 14-Dec-1997.)
a C b    ⇒   a C (b →4 a)
Theorem	u5lemc3 695	Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
a C b    ⇒   a C (b →5 a)
Theorem	u1lemc5 696	Commutation theorem for Sasaki implication. (Contributed by NM, 11-Jan-1998.)
a C b    ⇒   a C (a →1 b)
Theorem	u2lemc5 697	Commutation theorem for Dishkant implication. (Contributed by NM, 11-Jan-1998.)
a C b    ⇒   a C (a →2 b)
Theorem	u3lemc5 698	Commutation theorem for Kalmbach implication. (Contributed by NM, 11-Jan-1998.)
a C b    ⇒   a C (a →3 b)
Theorem	u4lemc5 699	Commutation theorem for non-tollens implication. (Contributed by NM, 11-Jan-1998.)
a C b    ⇒   a C (a →4 b)
Theorem	u5lemc5 700	Commutation theorem for relevance implication. (Contributed by NM, 11-Jan-1998.)
a C b    ⇒   a C (a →5 b)