[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 7 of 13)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Quantum Logic Explorer - 601-700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremu2lemaa 601 Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a2 b) ∩ a) = (ab)
 
Theoremu3lemaa 602 Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a3 b) ∩ a) = (a ∩ (ab))
 
Theoremu4lemaa 603 Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a4 b) ∩ a) = (ab)
 
Theoremu5lemaa 604 Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a5 b) ∩ a) = (ab)
 
Theoremu1lemana 605 Lemma for Sasaki implication study. (Contributed by NM, 14-Dec-1997.)
((a1 b) ∩ a ) = a
 
Theoremu2lemana 606 Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a2 b) ∩ a ) = ((ab) ∪ (ab ))
 
Theoremu3lemana 607 Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a3 b) ∩ a ) = ((ab) ∪ (ab ))
 
Theoremu4lemana 608 Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a4 b) ∩ a ) = ((ab) ∪ (ab ))
 
Theoremu5lemana 609 Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a5 b) ∩ a ) = ((ab) ∪ (ab ))
 
Theoremu1lemab 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.)
((a1 b) ∩ b) = ((ab) ∪ (ab))
 
Theoremu2lemab 611 Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a2 b) ∩ b) = b
 
Theoremu3lemab 612 Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a3 b) ∩ b) = ((ab) ∪ (ab))
 
Theoremu4lemab 613 Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a4 b) ∩ b) = ((ab) ∪ (ab))
 
Theoremu5lemab 614 Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a5 b) ∩ b) = ((ab) ∪ (ab))
 
Theoremu1lemanb 615 Lemma for Sasaki implication study. (Contributed by NM, 14-Dec-1997.)
((a1 b) ∩ b ) = (ab )
 
Theoremu2lemanb 616 Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a2 b) ∩ b ) = (ab )
 
Theoremu3lemanb 617 Lemma for Kalmbach implication study. (Contributed by NM, 14-Dec-1997.)
((a3 b) ∩ b ) = (ab )
 
Theoremu4lemanb 618 Lemma for non-tollens implication study. (Contributed by NM, 14-Dec-1997.)
((a4 b) ∩ b ) = ((ab) ∩ b )
 
Theoremu5lemanb 619 Lemma for relevance implication study. (Contributed by NM, 14-Dec-1997.)
((a5 b) ∩ b ) = (ab )
 
Theoremu1lemoa 620 Lemma for Sasaki implication study. (Contributed by NM, 14-Dec-1997.)
((a1 b) ∪ a) = 1
 
Theoremu2lemoa 621 Lemma for Dishkant implication study. (Contributed by NM, 14-Dec-1997.)
((a2 b) ∪ a) = 1
 
Theoremu3lemoa 622 Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a3 b) ∪ a) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu4lemoa 623 Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a4 b) ∪ a) = 1
 
Theoremu5lemoa 624 Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a5 b) ∪ a) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu1lemona 625 Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a1 b) ∪ a ) = (a ∪ (ab))
 
Theoremu2lemona 626 Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a2 b) ∪ a ) = (ab)
 
Theoremu3lemona 627 Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a3 b) ∪ a ) = (ab)
 
Theoremu4lemona 628 Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a4 b) ∪ a ) = (ab)
 
Theoremu5lemona 629 Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a5 b) ∪ a ) = (a ∪ (ab))
 
Theoremu1lemob 630 Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a1 b) ∪ b) = (ab)
 
Theoremu2lemob 631 Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a2 b) ∪ b) = ((ab ) ∪ b)
 
Theoremu3lemob 632 Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a3 b) ∪ b) = (ab)
 
Theoremu4lemob 633 Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a4 b) ∪ b) = (ab)
 
Theoremu5lemob 634 Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a5 b) ∪ b) = ((ab ) ∪ b)
 
Theoremu1lemonb 635 Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a1 b) ∪ b ) = 1
 
Theoremu2lemonb 636 Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a2 b) ∪ b ) = 1
 
Theoremu3lemonb 637 Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a3 b) ∪ b ) = 1
 
Theoremu4lemonb 638 Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a4 b) ∪ b ) = (((ab) ∪ (ab)) ∪ b )
 
Theoremu5lemonb 639 Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a5 b) ∪ b ) = (((ab) ∪ (ab)) ∪ b )
 
Theoremu1lemnaa 640 Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a1 b)a) = (a ∩ (ab ))
 
Theoremu2lemnaa 641 Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a2 b)a) = (ab )
 
Theoremu3lemnaa 642 Lemma for Kalmbach implication study. (Contributed by NM, 15-Dec-1997.)
((a3 b)a) = (ab )
 
Theoremu4lemnaa 643 Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a4 b)a) = (ab )
 
Theoremu5lemnaa 644 Lemma for relevance implication study. (Contributed by NM, 15-Dec-1997.)
((a5 b)a) = (a ∩ (ab ))
 
Theoremu1lemnana 645 Lemma for Sasaki implication study. (Contributed by NM, 15-Dec-1997.)
((a1 b)a ) = 0
 
Theoremu2lemnana 646 Lemma for Dishkant implication study. (Contributed by NM, 15-Dec-1997.)
((a2 b)a ) = 0
 
Theoremu3lemnana 647 Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b)a ) = (a ∩ ((ab) ∩ (ab )))
 
Theoremu4lemnana 648 Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
((a4 b)a ) = 0
 
Theoremu5lemnana 649 Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b)a ) = (a ∩ ((ab) ∩ (ab )))
 
Theoremu1lemnab 650 Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a1 b)b) = 0
 
Theoremu2lemnab 651 Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a2 b)b) = 0
 
Theoremu3lemnab 652 Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b)b) = 0
 
Theoremu4lemnab 653 Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b)b) = (((ab ) ∩ (ab )) ∩ b)
 
Theoremu5lemnab 654 Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b)b) = (((ab ) ∩ (ab )) ∩ b)
 
Theoremu1lemnanb 655 Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a1 b)b ) = (ab )
 
Theoremu2lemnanb 656 Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a2 b)b ) = ((ab) ∩ b )
 
Theoremu3lemnanb 657 Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b)b ) = (ab )
 
Theoremu4lemnanb 658 Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b)b ) = (ab )
 
Theoremu5lemnanb 659 Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b)b ) = ((ab) ∩ b )
 
Theoremu1lemnoa 660 Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a1 b)a) = a
 
Theoremu2lemnoa 661 Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a2 b)a) = ((ab) ∩ (ab ))
 
Theoremu3lemnoa 662 Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b)a) = ((ab) ∩ (ab ))
 
Theoremu4lemnoa 663 Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b)a) = ((ab) ∩ (ab ))
 
Theoremu5lemnoa 664 Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b)a) = ((ab) ∩ (ab ))
 
Theoremu1lemnona 665 Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a1 b)a ) = (ab )
 
Theoremu2lemnona 666 Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a2 b)a ) = (ab )
 
Theoremu3lemnona 667 Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b)a ) = (a ∪ (ab ))
 
Theoremu4lemnona 668 Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b)a ) = (ab )
 
Theoremu5lemnona 669 Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b)a ) = (ab )
 
Theoremu1lemnob 670 Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a1 b)b) = (ab)
 
Theoremu2lemnob 671 Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a2 b)b) = (ab)
 
Theoremu3lemnob 672 Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b)b) = (ab)
 
Theoremu4lemnob 673 Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b)b) = ((ab ) ∪ b)
 
Theoremu5lemnob 674 Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b)b) = (ab)
 
Theoremu1lemnonb 675 Lemma for Sasaki implication study. (Contributed by NM, 16-Dec-1997.)
((a1 b)b ) = ((ab ) ∩ (ab ))
 
Theoremu2lemnonb 676 Lemma for Dishkant implication study. (Contributed by NM, 16-Dec-1997.)
((a2 b)b ) = b
 
Theoremu3lemnonb 677 Lemma for Kalmbach implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b)b ) = ((ab ) ∩ (ab ))
 
Theoremu4lemnonb 678 Lemma for non-tollens implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b)b ) = ((ab ) ∩ (ab ))
 
Theoremu5lemnonb 679 Lemma for relevance implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b)b ) = ((ab ) ∩ (ab ))
 
Theoremu1lemc1 680 Commutation theorem for Sasaki implication. (Contributed by NM, 14-Dec-1997.)
a C (a1 b)
 
Theoremu2lemc1 681 Commutation theorem for Dishkant implication. (Contributed by NM, 14-Dec-1997.)
b C (a2 b)
 
Theoremu3lemc1 682 Commutation theorem for Kalmbach implication. (Contributed by NM, 14-Dec-1997.)
a C (a3 b)
 
Theoremu4lemc1 683 Commutation theorem for non-tollens implication. (Contributed by NM, 14-Dec-1997.)
b C (a4 b)
 
Theoremu5lemc1 684 Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
a C (a5 b)
 
Theoremu5lemc1b 685 Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
b C (a5 b)
 
Theoremu1lemc2 686 Commutation theorem for Sasaki implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c       a C (b1 c)
 
Theoremu2lemc2 687 Commutation theorem for Dishkant implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c       a C (b2 c)
 
Theoremu3lemc2 688 Commutation theorem for Kalmbach implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c       a C (b3 c)
 
Theoremu4lemc2 689 Commutation theorem for non-tollens implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c       a C (b4 c)
 
Theoremu5lemc2 690 Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
a C b    &   a C c       a C (b5 c)
 
Theoremu1lemc3 691 Commutation theorem for Sasaki implication. (Contributed by NM, 14-Dec-1997.)
a C b       a C (b1 a)
 
Theoremu2lemc3 692 Commutation theorem for Dishkant implication. (Contributed by NM, 14-Dec-1997.)
a C b       a C (b2 a)
 
Theoremu3lemc3 693 Commutation theorem for Kalmbach implication. (Contributed by NM, 14-Dec-1997.)
a C b       a C (b3 a)
 
Theoremu4lemc3 694 Commutation theorem for non-tollens implication. (Contributed by NM, 14-Dec-1997.)
a C b       a C (b4 a)
 
Theoremu5lemc3 695 Commutation theorem for relevance implication. (Contributed by NM, 14-Dec-1997.)
a C b       a C (b5 a)
 
Theoremu1lemc5 696 Commutation theorem for Sasaki implication. (Contributed by NM, 11-Jan-1998.)
a C b       a C (a1 b)
 
Theoremu2lemc5 697 Commutation theorem for Dishkant implication. (Contributed by NM, 11-Jan-1998.)
a C b       a C (a2 b)
 
Theoremu3lemc5 698 Commutation theorem for Kalmbach implication. (Contributed by NM, 11-Jan-1998.)
a C b       a C (a3 b)
 
Theoremu4lemc5 699 Commutation theorem for non-tollens implication. (Contributed by NM, 11-Jan-1998.)
a C b       a C (a4 b)
 
Theoremu5lemc5 700 Commutation theorem for relevance implication. (Contributed by NM, 11-Jan-1998.)
a C b       a C (a5 b)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1217
  Copyright terms: Public domain < Previous  Next >