[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 7 of 13) 		< Previous  Next >
Browser slow? Try the
Unicode 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.
((a ->2 b) ^ a) = (a ^ b)
 
Theoremu3lemaa 602 Lemma for Kalmbach implication study.
((a ->3 b) ^ a) = (a ^ (a' v b))
 
Theoremu4lemaa 603 Lemma for non-tollens implication study.
((a ->4 b) ^ a) = (a ^ b)
 
Theoremu5lemaa 604 Lemma for relevance implication study.
((a ->5 b) ^ a) = (a ^ b)
 
Theoremu1lemana 605 Lemma for Sasaki implication study.
((a ->1 b) ^ a') = a'
 
Theoremu2lemana 606 Lemma for Dishkant implication study.
((a ->2 b) ^ a') = ((a' ^ b) v (a' ^ b'))
 
Theoremu3lemana 607 Lemma for Kalmbach implication study.
((a ->3 b) ^ a') = ((a' ^ b) v (a' ^ b'))
 
Theoremu4lemana 608 Lemma for non-tollens implication study.
((a ->4 b) ^ a') = ((a' ^ b) v (a' ^ b'))
 
Theoremu5lemana 609 Lemma for relevance implication study.
((a ->5 b) ^ a') = ((a' ^ b) v (a' ^ b'))
 
Theoremu1lemab 610 Lemma for Sasaki implication study. Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation.
((a ->1 b) ^ b) = ((a ^ b) v (a' ^ b))
 
Theoremu2lemab 611 Lemma for Dishkant implication study.
((a ->2 b) ^ b) = b
 
Theoremu3lemab 612 Lemma for Kalmbach implication study.
((a ->3 b) ^ b) = ((a ^ b) v (a' ^ b))
 
Theoremu4lemab 613 Lemma for non-tollens implication study.
((a ->4 b) ^ b) = ((a ^ b) v (a' ^ b))
 
Theoremu5lemab 614 Lemma for relevance implication study.
((a ->5 b) ^ b) = ((a ^ b) v (a' ^ b))
 
Theoremu1lemanb 615 Lemma for Sasaki implication study.
((a ->1 b) ^ b') = (a' ^ b')
 
Theoremu2lemanb 616 Lemma for Dishkant implication study.
((a ->2 b) ^ b') = (a' ^ b')
 
Theoremu3lemanb 617 Lemma for Kalmbach implication study.
((a ->3 b) ^ b') = (a' ^ b')
 
Theoremu4lemanb 618 Lemma for non-tollens implication study.
((a ->4 b) ^ b') = ((a' v b) ^ b')
 
Theoremu5lemanb 619 Lemma for relevance implication study.
((a ->5 b) ^ b') = (a' ^ b')
 
Theoremu1lemoa 620 Lemma for Sasaki implication study.
((a ->1 b) v a) = 1
 
Theoremu2lemoa 621 Lemma for Dishkant implication study.
((a ->2 b) v a) = 1
 
Theoremu3lemoa 622 Lemma for Kalmbach implication study.
((a ->3 b) v a) = (a v ((a' ^ b) v (a' ^ b')))
 
Theoremu4lemoa 623 Lemma for non-tollens implication study.
((a ->4 b) v a) = 1
 
Theoremu5lemoa 624 Lemma for relevance implication study.
((a ->5 b) v a) = (a v ((a' ^ b) v (a' ^ b')))
 
Theoremu1lemona 625 Lemma for Sasaki implication study.
((a ->1 b) v a') = (a' v (a ^ b))
 
Theoremu2lemona 626 Lemma for Dishkant implication study.
((a ->2 b) v a') = (a' v b)
 
Theoremu3lemona 627 Lemma for Kalmbach implication study.
((a ->3 b) v a') = (a' v b)
 
Theoremu4lemona 628 Lemma for non-tollens implication study.
((a ->4 b) v a') = (a' v b)
 
Theoremu5lemona 629 Lemma for relevance implication study.
((a ->5 b) v a') = (a' v (a ^ b))
 
Theoremu1lemob 630 Lemma for Sasaki implication study.
((a ->1 b) v b) = (a' v b)
 
Theoremu2lemob 631 Lemma for Dishkant implication study.
((a ->2 b) v b) = ((a' ^ b') v b)
 
Theoremu3lemob 632 Lemma for Kalmbach implication study.
((a ->3 b) v b) = (a' v b)
 
Theoremu4lemob 633 Lemma for non-tollens implication study.
((a ->4 b) v b) = (a' v b)
 
Theoremu5lemob 634 Lemma for relevance implication study.
((a ->5 b) v b) = ((a' ^ b') v b)
 
Theoremu1lemonb 635 Lemma for Sasaki implication study.
((a ->1 b) v b') = 1
 
Theoremu2lemonb 636 Lemma for Dishkant implication study.
((a ->2 b) v b') = 1
 
Theoremu3lemonb 637 Lemma for Kalmbach implication study.
((a ->3 b) v b') = 1
 
Theoremu4lemonb 638 Lemma for non-tollens implication study.
((a ->4 b) v b') = (((a ^ b) v (a' ^ b)) v b')
 
Theoremu5lemonb 639 Lemma for relevance implication study.
((a ->5 b) v b') = (((a ^ b) v (a' ^ b)) v b')
 
Theoremu1lemnaa 640 Lemma for Sasaki implication study.
((a ->1 b)' ^ a) = (a ^ (a' v b'))
 
Theoremu2lemnaa 641 Lemma for Dishkant implication study.
((a ->2 b)' ^ a) = (a ^ b')
 
Theoremu3lemnaa 642 Lemma for Kalmbach implication study.
((a ->3 b)' ^ a) = (a ^ b')
 
Theoremu4lemnaa 643 Lemma for non-tollens implication study.
((a ->4 b)' ^ a) = (a ^ b')
 
Theoremu5lemnaa 644 Lemma for relevance implication study.
((a ->5 b)' ^ a) = (a ^ (a' v b'))
 
Theoremu1lemnana 645 Lemma for Sasaki implication study.
((a ->1 b)' ^ a') = 0
 
Theoremu2lemnana 646 Lemma for Dishkant implication study.
((a ->2 b)' ^ a') = 0
 
Theoremu3lemnana 647 Lemma for Kalmbach implication study.
((a ->3 b)' ^ a') = (a' ^ ((a v b) ^ (a v b')))
 
Theoremu4lemnana 648 Lemma for non-tollens implication study.
((a ->4 b)' ^ a') = 0
 
Theoremu5lemnana 649 Lemma for relevance implication study.
((a ->5 b)' ^ a') = (a' ^ ((a v b) ^ (a v b')))
 
Theoremu1lemnab 650 Lemma for Sasaki implication study.
((a ->1 b)' ^ b) = 0
 
Theoremu2lemnab 651 Lemma for Dishkant implication study.
((a ->2 b)' ^ b) = 0
 
Theoremu3lemnab 652 Lemma for Kalmbach implication study.
((a ->3 b)' ^ b) = 0
 
Theoremu4lemnab 653 Lemma for non-tollens implication study.
((a ->4 b)' ^ b) = (((a v b') ^ (a' v b')) ^ b)
 
Theoremu5lemnab 654 Lemma for relevance implication study.
((a ->5 b)' ^ b) = (((a v b') ^ (a' v b')) ^ b)
 
Theoremu1lemnanb 655 Lemma for Sasaki implication study.
((a ->1 b)' ^ b') = (a ^ b')
 
Theoremu2lemnanb 656 Lemma for Dishkant implication study.
((a ->2 b)' ^ b') = ((a v b) ^ b')
 
Theoremu3lemnanb 657 Lemma for Kalmbach implication study.
((a ->3 b)' ^ b') = (a ^ b')
 
Theoremu4lemnanb 658 Lemma for non-tollens implication study.
((a ->4 b)' ^ b') = (a ^ b')
 
Theoremu5lemnanb 659 Lemma for relevance implication study.
((a ->5 b)' ^ b') = ((a v b) ^ b')
 
Theoremu1lemnoa 660 Lemma for Sasaki implication study.
((a ->1 b)' v a) = a
 
Theoremu2lemnoa 661 Lemma for Dishkant implication study.
((a ->2 b)' v a) = ((a v b) ^ (a v b'))
 
Theoremu3lemnoa 662 Lemma for Kalmbach implication study.
((a ->3 b)' v a) = ((a v b) ^ (a v b'))
 
Theoremu4lemnoa 663 Lemma for non-tollens implication study.
((a ->4 b)' v a) = ((a v b) ^ (a v b'))
 
Theoremu5lemnoa 664 Lemma for relevance implication study.
((a ->5 b)' v a) = ((a v b) ^ (a v b'))
 
Theoremu1lemnona 665 Lemma for Sasaki implication study.
((a ->1 b)' v a') = (a' v b')
 
Theoremu2lemnona 666 Lemma for Dishkant implication study.
((a ->2 b)' v a') = (a' v b')
 
Theoremu3lemnona 667 Lemma for Kalmbach implication study.
((a ->3 b)' v a') = (a' v (a ^ b'))
 
Theoremu4lemnona 668 Lemma for non-tollens implication study.
((a ->4 b)' v a') = (a' v b')
 
Theoremu5lemnona 669 Lemma for relevance implication study.
((a ->5 b)' v a') = (a' v b')
 
Theoremu1lemnob 670 Lemma for Sasaki implication study.
((a ->1 b)' v b) = (a v b)
 
Theoremu2lemnob 671 Lemma for Dishkant implication study.
((a ->2 b)' v b) = (a v b)
 
Theoremu3lemnob 672 Lemma for Kalmbach implication study.
((a ->3 b)' v b) = (a v b)
 
Theoremu4lemnob 673 Lemma for non-tollens implication study.
((a ->4 b)' v b) = ((a ^ b') v b)
 
Theoremu5lemnob 674 Lemma for relevance implication study.
((a ->5 b)' v b) = (a v b)
 
Theoremu1lemnonb 675 Lemma for Sasaki implication study.
((a ->1 b)' v b') = ((a v b') ^ (a' v b'))
 
Theoremu2lemnonb 676 Lemma for Dishkant implication study.
((a ->2 b)' v b') = b'
 
Theoremu3lemnonb 677 Lemma for Kalmbach implication study.
((a ->3 b)' v b') = ((a v b') ^ (a' v b'))
 
Theoremu4lemnonb 678 Lemma for non-tollens implication study.
((a ->4 b)' v b') = ((a v b') ^ (a' v b'))
 
Theoremu5lemnonb 679 Lemma for relevance implication study.
((a ->5 b)' v b') = ((a v b') ^ (a' v b'))
 
Theoremu1lemc1 680 Commutation theorem for Sasaki implication.
a C (a ->1 b)
 
Theoremu2lemc1 681 Commutation theorem for Dishkant implication.
b C (a ->2 b)
 
Theoremu3lemc1 682 Commutation theorem for Kalmbach implication.
a C (a ->3 b)
 
Theoremu4lemc1 683 Commutation theorem for non-tollens implication.
b C (a ->4 b)
 
Theoremu5lemc1 684 Commutation theorem for relevance implication.
a C (a ->5 b)
 
Theoremu5lemc1b 685 Commutation theorem for relevance implication.
b C (a ->5 b)
 
Theoremu1lemc2 686 Commutation theorem for Sasaki implication.
a C b   &   a C c   =>   a C (b ->1 c)
 
Theoremu2lemc2 687 Commutation theorem for Dishkant implication.
a C b   &   a C c   =>   a C (b ->2 c)
 
Theoremu3lemc2 688 Commutation theorem for Kalmbach implication.
a C b   &   a C c   =>   a C (b ->3 c)
 
Theoremu4lemc2 689 Commutation theorem for non-tollens implication.
a C b   &   a C c   =>   a C (b ->4 c)
 
Theoremu5lemc2 690 Commutation theorem for relevance implication.
a C b   &   a C c   =>   a C (b ->5 c)
 
Theoremu1lemc3 691 Commutation theorem for Sasaki implication.
a C b   =>   a C (b ->1 a)
 
Theoremu2lemc3 692 Commutation theorem for Dishkant implication.
a C b   =>   a C (b ->2 a)
 
Theoremu3lemc3 693 Commutation theorem for Kalmbach implication.
a C b   =>   a C (b ->3 a)
 
Theoremu4lemc3 694 Commutation theorem for non-tollens implication.
a C b   =>   a C (b ->4 a)
 
Theoremu5lemc3 695 Commutation theorem for relevance implication.
a C b   =>   a C (b ->5 a)
 
Theoremu1lemc5 696 Commutation theorem for Sasaki implication.
a C b   =>   a C (a ->1 b)
 
Theoremu2lemc5 697 Commutation theorem for Dishkant implication.
a C b   =>   a C (a ->2 b)
 
Theoremu3lemc5 698 Commutation theorem for Kalmbach implication.
a C b   =>   a C (a ->3 b)
 
Theoremu4lemc5 699 Commutation theorem for non-tollens implication.
a C b   =>   a C (a ->4 b)
 
Theoremu5lemc5 700 Commutation theorem for relevance implication.
a C b   =>   a C (a ->5 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-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215
  Copyright terms: Public domain < Previous  Next >