[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 6 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 - 501-600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremi3n2 501 Equivalence for Kalmbach implication.
(a' ->3 b') = ((a ^ b) v ((a v b') ^ (a' v (a ^ b'))))
 
Theoremni32 502 Equivalence for Kalmbach implication.
(a ->3 b)' = ((a v b) ^ ((a ^ b') v (a' ^ (a v b'))))
 
Theoremoi3ai3 503 Theorem for Kalmbach implication.
((a ^ b) v (a ->3 b)') = ((a v b) ^ (a' ->3 b'))
 
Theoremi3lem1 504 Lemma for Kalmbach implication.
(a ->3 b) = 1   =>   ((a' ^ b) v (a' ^ b')) = a'
 
Theoremi3lem2 505 Lemma for Kalmbach implication.
(a ->3 b) = 1   =>   a C b
 
Theoremi3lem3 506 Lemma for Kalmbach implication.
(a ->3 b) = 1   =>   ((a' v b) ^ b') = (a' ^ b')
 
Theoremi3lem4 507 Lemma for Kalmbach implication.
(a ->3 b) = 1   =>   (a' v b) = 1
 
Theoremcomi31 508 Commutation theorem.
a C (a ->3 b)
 
Theoremcom2i3 509 Commutation theorem.
a C b   &   a C c   =>   a C (b ->3 c)
 
Theoremcomi32 510 Commutation theorem.
a C b   =>   a C (b ->3 a)
 
Theoremlem4 511 Lemma 4 of Kalmbach p. 240.
(a ->3 (a ->3 b)) = (a' v b)
 
Theoremi0i3 512 Translation to Kalmbach implication.
(a' v b) = 1   =>   (a ->3 (a ->3 b)) = 1
 
Theoremi3i0 513 Translation from Kalmbach implication.
(a ->3 (a ->3 b)) = 1   =>   (a' v b) = 1
 
Theoremska14 514 Soundness proof for KA14.
((a' v b) ->3 (a ->3 (a ->3 b))) = 1
 
Theoremi3le 515 L.e. to Kalmbach implication.
(a ->3 b) = 1   =>   a =< b
 
Theorembii3 516 Biconditional implies Kalmbach implication.
((a == b) ->3 (a ->3 b)) = 1
 
Theorembinr1 517 Pavicic binary logic ax-r1 analog.
(a ->3 b) = 1   =>   (b' ->3 a') = 1
 
Theorembinr2 518 Pavicic binary logic ax-r2 analog.
(a ->3 b) = 1   &   (b ->3 c) = 1   =>   (a ->3 c) = 1
 
Theorembinr3 519 Pavicic binary logic axr3 analog.
(a ->3 c) = 1   &   (b ->3 c) = 1   =>   ((a v b) ->3 c) = 1
 
Theoremi31 520 Theorem for Kalmbach implication.
(a ->3 1) = 1
 
Theoremi3aa 521 Add antecedent.
a = 1   =>   (b ->3 a) = 1
 
Theoremi3abs1 522 Antecedent absorption.
(a ->3 (a ->3 (a ->3 b))) = (a ->3 (a ->3 b))
 
Theoremi3abs2 523 Antecedent absorption.
(a ->3 (a ->3 (a ->3 b))) = 1   =>   (a ->3 (a ->3 b)) = 1
 
Theoremi3abs3 524 Antecedent absorption.
((a ->3 b) ->3 ((a ->3 b) ->3 a)) = ((a ->3 b) ->3 a)
 
Theoremi3orcom 525 Commutative law for conjunction with Kalmbach implication.
((a v b) ->3 (b v a)) = 1
 
Theoremi3ancom 526 Commutative law for disjunction with Kalmbach implication.
((a ^ b) ->3 (b ^ a)) = 1
 
Theorembi3tr 527 Transitive inference.
a = b   &   (b ->3 c) = 1   =>   (a ->3 c) = 1
 
Theoremi3btr 528 Transitive inference.
(a ->3 b) = 1   &   b = c   =>   (a ->3 c) = 1
 
Theoremi33tr1 529 Transitive inference useful for introducing definitions.
(a ->3 b) = 1   &   c = a   &   d = b   =>   (c ->3 d) = 1
 
Theoremi33tr2 530 Transitive inference useful for eliminating definitions.
(a ->3 b) = 1   &   a = c   &   b = d   =>   (c ->3 d) = 1
 
Theoremi3con1 531 Contrapositive.
(a' ->3 b') = 1   =>   (b ->3 a) = 1
 
Theoremi3ror 532 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((a v c) ->3 (b v c)) = 1
 
Theoremi3lor 533 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((c v a) ->3 (c v b)) = 1
 
Theoremi32or 534 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (c ->3 d) = 1   =>   ((a v c) ->3 (b v d)) = 1
 
Theoremi3ran 535 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((a ^ c) ->3 (b ^ c)) = 1
 
Theoremi3lan 536 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((c ^ a) ->3 (c ^ b)) = 1
 
Theoremi32an 537 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (c ->3 d) = 1   =>   ((a ^ c) ->3 (b ^ d)) = 1
 
Theoremi3ri3 538 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (b ->3 a) = 1   =>   ((a ->3 c) ->3 (b ->3 c)) = 1
 
Theoremi3li3 539 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (b ->3 a) = 1   =>   ((c ->3 a) ->3 (c ->3 b)) = 1
 
Theoremi32i3 540 WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (b ->3 a) = 1   &   (c ->3 d) = 1   &   (d ->3 c) = 1   =>   ((a ->3 c) ->3 (b ->3 d)) = 1
 
Theoremi0i3tr 541 Transitive inference.
(a ->3 (a ->3 b)) = 1   &   (b ->3 c) = 1   =>   (a ->3 (a ->3 c)) = 1
 
Theoremi3i0tr 542 Transitive inference.
(a ->3 b) = 1   &   (b ->3 (b ->3 c)) = 1   =>   (a ->3 (a ->3 c)) = 1
 
Theoremi3th1 543 Theorem for Kalmbach implication.
(a ->3 (a ->3 (b ->3 a))) = 1
 
Theoremi3th2 544 Theorem for Kalmbach implication.
(a ->3 (b ->3 (b ->3 a))) = 1
 
Theoremi3th3 545 Theorem for Kalmbach implication.
(a' ->3 (a ->3 (a ->3 b))) = 1
 
Theoremi3th4 546 Theorem for Kalmbach implication.
(a ->3 (b ->3 b)) = 1
 
Theoremi3th5 547 Theorem for Kalmbach implication.
((a ->3 b) ->3 (a ->3 (a ->3 b))) = 1
 
Theoremi3th6 548 Theorem for Kalmbach implication.
((a ->3 (a ->3 (a ->3 b))) ->3 (a ->3 (a ->3 b))) = 1
 
Theoremi3th7 549 Theorem for Kalmbach implication.
(a ->3 ((a ->3 b) ->3 a)) = 1
 
Theoremi3th8 550 Theorem for Kalmbach implication.
((a ->3 b)' ->3 ((a ->3 b) ->3 a)) = 1
 
Theoremi3con 551 Theorem for Kalmbach implication.
((a ->3 b) ->3 ((a ->3 b) ->3 (b' ->3 a'))) = 1
 
Theoremi3orlem1 552 Lemma for Kalmbach implication OR builder.
((a v c) ^ ((a v c)' v (b v c))) =< ((a v c) ->3 (b v c))
 
Theoremi3orlem2 553 Lemma for Kalmbach implication OR builder.
(a ^ b) =< ((a v c) ->3 (b v c))
 
Theoremi3orlem3 554 Lemma for Kalmbach implication OR builder.
c =< ((a v c) ->3 (b v c))
 
Theoremi3orlem4 555 Lemma for Kalmbach implication OR builder.
((a v c)' ^ (b v c)) =< ((a v c) ->3 (b v c))
 
Theoremi3orlem5 556 Lemma for Kalmbach implication OR builder.
((a' ^ b') ^ c') =< ((a v c) ->3 (b v c))
 
Theoremi3orlem6 557 Lemma for Kalmbach implication OR builder.
((a ->3 b)' v ((a v c) ->3 (b v c))) = (((a v b) ^ (a' ->3 b')) v ((a v c) ->3 (b v c)))
 
Theoremi3orlem7 558 Lemma for Kalmbach implication OR builder.
(a ^ b') =< ((a ->3 b)' v ((a v c) ->3 (b v c)))
 
Theoremi3orlem8 559 Lemma for Kalmbach implication OR builder.
(((a v b) ^ (a v b')) ^ a') =< ((a ->3 b)' v ((a v c) ->3 (b v c)))
 
0.3.5  Unified disjunction
 
Theoremud1lem1 560 Lemma for unified disjunction.
((a ->1 b) ->1 (b ->1 a)) = (a v (a' ^ b'))
 
Theoremud1lem2 561 Lemma for unified disjunction.
((a v (a' ^ b')) ->1 a) = (a v b)
 
Theoremud1lem3 562 Lemma for unified disjunction.
((a ->1 b) ->1 (a v b)) = (a v b)
 
Theoremud2lem1 563 Lemma for unified disjunction.
((a ->2 b) ->2 (b ->2 a)) = (a v (a' ^ b'))
 
Theoremud2lem2 564 Lemma for unified disjunction.
((a v (a' ^ b')) ->2 a) = (a v b)
 
Theoremud2lem3 565 Lemma for unified disjunction.
((a ->2 b) ->2 (a v b)) = (a v b)
 
Theoremud3lem1a 566 Lemma for unified disjunction.
((a ->3 b)' ^ (b ->3 a)) = (a ^ b')
 
Theoremud3lem1b 567 Lemma for unified disjunction.
((a ->3 b)' ^ (b ->3 a)') = 0
 
Theoremud3lem1c 568 Lemma for unified disjunction.
((a ->3 b)' v (b ->3 a)) = (a v b')
 
Theoremud3lem1d 569 Lemma for unified disjunction.
((a ->3 b) ^ ((a ->3 b)' v (b ->3 a))) = ((a' ^ b') v (a ^ (a' v b)))
 
Theoremud3lem1 570 Lemma for unified disjunction.
((a ->3 b) ->3 (b ->3 a)) = (a v (a' ^ b'))
 
Theoremud3lem2 571 Lemma for unified disjunction.
((a v (a' ^ b')) ->3 a) = (a v b)
 
Theoremud3lem3a 572 Lemma for unified disjunction.
((a ->3 b)' ^ (a v b)) = (a ->3 b)'
 
Theoremud3lem3b 573 Lemma for unified disjunction.
((a ->3 b)' ^ (a v b)') = 0
 
Theoremud3lem3c 574 Lemma for unified disjunction.
((a ->3 b)' v (a v b)) = (a v b)
 
Theoremud3lem3d 575 Lemma for unified disjunction.
((a ->3 b) ^ ((a ->3 b)' v (a v b))) = ((a' ^ b) v (a ^ (a' v b)))
 
Theoremud3lem3 576 Lemma for unified disjunction.
((a ->3 b) ->3 (a v b)) = (a v b)
 
Theoremud4lem1a 577 Lemma for unified disjunction.
((a ->4 b) ^ (b ->4 a)) = ((a ^ b) v (a' ^ b'))
 
Theoremud4lem1b 578 Lemma for unified disjunction.
((a ->4 b)' ^ (b ->4 a)) = (a ^ b')
 
Theoremud4lem1c 579 Lemma for unified disjunction.
((a ->4 b)' v (b ->4 a)) = (a v b')
 
Theoremud4lem1d 580 Lemma for unified disjunction.
(((a ->4 b)' v (b ->4 a)) ^ (b ->4 a)') = (((a' v b') ^ (a' v b)) ^ a)
 
Theoremud4lem1 581 Lemma for unified disjunction.
((a ->4 b) ->4 (b ->4 a)) = (a v (a' ^ b'))
 
Theoremud4lem2 582 Lemma for unified disjunction.
((a v (a' ^ b')) ->4 a) = (a v b)
 
Theoremud4lem3a 583 Lemma for unified disjunction.
((a ->4 b)' ^ (a v b)) = (a ->4 b)'
 
Theoremud4lem3b 584 Lemma for unified disjunction.
((a ->4 b)' v (a v b)) = (a v b)
 
Theoremud4lem3 585 Lemma for unified disjunction.
((a ->4 b) ->4 (a v b)) = (a v b)
 
Theoremud5lem1a 586 Lemma for unified disjunction.
((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a' ^ b'))
 
Theoremud5lem1b 587 Lemma for unified disjunction.
((a ->5 b)' ^ (b ->5 a)) = (a ^ b')
 
Theoremud5lem1c 588 Lemma for unified disjunction.
((a ->5 b)' ^ (b ->5 a)') = (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b')))
 
Theoremud5lem1 589 Lemma for unified disjunction.
((a ->5 b) ->5 (b ->5 a)) = (a v b')
 
Theoremud5lem2 590 Lemma for unified disjunction.
((a v b') ->5 a) = (a v (a' ^ b))
 
Theoremud5lem3a 591 Lemma for unified disjunction.
((a ->5 b) ^ (a v (a' ^ b))) = ((a ^ b) v (a' ^ b))
 
Theoremud5lem3b 592 Lemma for unified disjunction.
((a ->5 b)' ^ (a v (a' ^ b))) = (a ^ (a' v b'))
 
Theoremud5lem3c 593 Lemma for unified disjunction.
((a ->5 b)' ^ (a v (a' ^ b))') = (((a v b) ^ (a v b')) ^ a')
 
Theoremud5lem3 594 Lemma for unified disjunction.
((a ->5 b) ->5 (a v (a' ^ b))) = (a v b)
 
Theoremud1 595 Unified disjunction for Sasaki implication.
(a v b) = ((a ->1 b) ->1 (((a ->1 b) ->1 (b ->1 a)) ->1 a))
 
Theoremud2 596 Unified disjunction for Dishkant implication.
(a v b) = ((a ->2 b) ->2 (((a ->2 b) ->2 (b ->2 a)) ->2 a))
 
Theoremud3 597 Unified disjunction for Kalmbach implication.
(a v b) = ((a ->3 b) ->3 (((a ->3 b) ->3 (b ->3 a)) ->3 a))
 
Theoremud4 598 Unified disjunction for non-tollens implication.
(a v b) = ((a ->4 b) ->4 (((a ->4 b) ->4 (b ->4 a)) ->4 a))
 
Theoremud5 599 Unified disjunction for relevance implication.
(a v b) = ((a ->5 b) ->5 (((a ->5 b) ->5 (b ->5 a)) ->5 a))
 
0.3.6  Lemmas for unified implication study
 
Theoremu1lemaa 600 Lemma for Sasaki implication study. Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation.
((a ->1 b) ^ a) = (a ^ 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 >