 Home Quantum Logic ExplorerTheorem List (p. 6 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 - 501-600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremi3n2 501 Equivalence for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(a3 b ) = ((ab) ∪ ((ab ) ∩ (a ∪ (ab ))))

Theoremni32 502 Equivalence for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(a3 b) = ((ab) ∩ ((ab ) ∪ (a ∩ (ab ))))

Theoremoi3ai3 503 Theorem for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
((ab) ∪ (a3 b) ) = ((ab) ∩ (a3 b ))

Theoremi3lem1 504 Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       ((ab) ∪ (ab )) = a

Theoremi3lem2 505 Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       a C b

Theoremi3lem3 506 Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       ((ab) ∩ b ) = (ab )

Theoremi3lem4 507 Lemma for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       (ab) = 1

Theoremcomi31 508 Commutation theorem. (Contributed by NM, 9-Nov-1997.)
a C (a3 b)

Theoremcom2i3 509 Commutation theorem. (Contributed by NM, 9-Nov-1997.)
a C b    &   a C c       a C (b3 c)

Theoremcomi32 510 Commutation theorem. (Contributed by NM, 9-Nov-1997.)
a C b       a C (b3 a)

Theoremlem4 511 Lemma 4 of Kalmbach p. 240. (Contributed by NM, 5-Nov-1997.)
(a3 (a3 b)) = (ab)

Theoremi0i3 512 Translation to Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(ab) = 1       (a3 (a3 b)) = 1

Theoremi3i0 513 Translation from Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
(a3 (a3 b)) = 1       (ab) = 1

Theoremska14 514 Soundness proof for KA14. (Contributed by NM, 3-Nov-1997.)
((ab) →3 (a3 (a3 b))) = 1

Theoremi3le 515 L.e. to Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       ab

Theorembii3 516 Biconditional implies Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
((ab) →3 (a3 b)) = 1

Theorembinr1 517 Pavicic binary logic ax-r1 analog. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       (b3 a ) = 1

Theorembinr2 518 Pavicic binary logic ax-r2 analog. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   (b3 c) = 1       (a3 c) = 1

Theorembinr3 519 Pavicic binary logic axr3 analog. (Contributed by NM, 7-Nov-1997.)
(a3 c) = 1    &   (b3 c) = 1       ((ab) →3 c) = 1

Theoremi31 520 Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 1) = 1

Theoremi3aa 521 Add antecedent. (Contributed by NM, 7-Nov-1997.)
a = 1       (b3 a) = 1

Theoremi3abs1 522 Antecedent absorption. (Contributed by NM, 16-Nov-1997.)
(a3 (a3 (a3 b))) = (a3 (a3 b))

Theoremi3abs2 523 Antecedent absorption. (Contributed by NM, 9-Nov-1997.)
(a3 (a3 (a3 b))) = 1       (a3 (a3 b)) = 1

Theoremi3abs3 524 Antecedent absorption. (Contributed by NM, 19-Nov-1997.)
((a3 b) →3 ((a3 b) →3 a)) = ((a3 b) →3 a)

Theoremi3orcom 525 Commutative law for conjunction with Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
((ab) →3 (ba)) = 1

Theoremi3ancom 526 Commutative law for disjunction with Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
((ab) →3 (ba)) = 1

Theorembi3tr 527 Transitive inference. (Contributed by NM, 7-Nov-1997.)
a = b    &   (b3 c) = 1       (a3 c) = 1

Theoremi3btr 528 Transitive inference. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   b = c       (a3 c) = 1

Theoremi33tr1 529 Transitive inference useful for introducing definitions. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   c = a    &   d = b       (c3 d) = 1

Theoremi33tr2 530 Transitive inference useful for eliminating definitions. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   a = c    &   b = d       (c3 d) = 1

Theoremi3con1 531 Contrapositive. (Contributed by NM, 7-Nov-1997.)
(a3 b ) = 1       (b3 a) = 1

Theoremi3ror 532 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       ((ac) →3 (bc)) = 1

Theoremi3lor 533 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       ((ca) →3 (cb)) = 1

Theoremi32or 534 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   (c3 d) = 1       ((ac) →3 (bd)) = 1

Theoremi3ran 535 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       ((ac) →3 (bc)) = 1

Theoremi3lan 536 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1       ((ca) →3 (cb)) = 1

Theoremi32an 537 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   (c3 d) = 1       ((ac) →3 (bd)) = 1

Theoremi3ri3 538 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   (b3 a) = 1       ((a3 c) →3 (b3 c)) = 1

Theoremi3li3 539 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   (b3 a) = 1       ((c3 a) →3 (c3 b)) = 1

Theoremi32i3 540 WQL (Weak Quantum Logic) rule. (Contributed by NM, 7-Nov-1997.)
(a3 b) = 1    &   (b3 a) = 1    &   (c3 d) = 1    &   (d3 c) = 1       ((a3 c) →3 (b3 d)) = 1

Theoremi0i3tr 541 Transitive inference. (Contributed by NM, 9-Nov-1997.)
(a3 (a3 b)) = 1    &   (b3 c) = 1       (a3 (a3 c)) = 1

Theoremi3i0tr 542 Transitive inference. (Contributed by NM, 9-Nov-1997.)
(a3 b) = 1    &   (b3 (b3 c)) = 1       (a3 (a3 c)) = 1

Theoremi3th1 543 Theorem for Kalmbach implication. (Contributed by NM, 16-Nov-1997.)
(a3 (a3 (b3 a))) = 1

Theoremi3th2 544 Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 (b3 (b3 a))) = 1

Theoremi3th3 545 Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 (a3 (a3 b))) = 1

Theoremi3th4 546 Theorem for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 (b3 b)) = 1

Theoremi3th5 547 Theorem for Kalmbach implication. (Contributed by NM, 16-Nov-1997.)
((a3 b) →3 (a3 (a3 b))) = 1

Theoremi3th6 548 Theorem for Kalmbach implication. (Contributed by NM, 16-Nov-1997.)
((a3 (a3 (a3 b))) →3 (a3 (a3 b))) = 1

Theoremi3th7 549 Theorem for Kalmbach implication. (Contributed by NM, 19-Nov-1997.)
(a3 ((a3 b) →3 a)) = 1

Theoremi3th8 550 Theorem for Kalmbach implication. (Contributed by NM, 19-Nov-1997.)
((a3 b)3 ((a3 b) →3 a)) = 1

Theoremi3con 551 Theorem for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
((a3 b) →3 ((a3 b) →3 (b3 a ))) = 1

Theoremi3orlem1 552 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((ac) ∩ ((ac) ∪ (bc))) ≤ ((ac) →3 (bc))

Theoremi3orlem2 553 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
(ab) ≤ ((ac) →3 (bc))

Theoremi3orlem3 554 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
c ≤ ((ac) →3 (bc))

Theoremi3orlem4 555 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((ac) ∩ (bc)) ≤ ((ac) →3 (bc))

Theoremi3orlem5 556 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((ab ) ∩ c ) ≤ ((ac) →3 (bc))

Theoremi3orlem6 557 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
((a3 b) ∪ ((ac) →3 (bc))) = (((ab) ∩ (a3 b )) ∪ ((ac) →3 (bc)))

Theoremi3orlem7 558 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
(ab ) ≤ ((a3 b) ∪ ((ac) →3 (bc)))

Theoremi3orlem8 559 Lemma for Kalmbach implication OR builder. (Contributed by NM, 11-Nov-1997.)
(((ab) ∩ (ab )) ∩ a ) ≤ ((a3 b) ∪ ((ac) →3 (bc)))

0.3.5  Unified disjunction

Theoremud1lem1 560 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a1 b) →1 (b1 a)) = (a ∪ (ab ))

Theoremud1lem2 561 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (ab )) →1 a) = (ab)

Theoremud1lem3 562 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a1 b) →1 (ab)) = (ab)

Theoremud2lem1 563 Lemma for unified disjunction. (Contributed by NM, 22-Nov-1997.)
((a2 b) →2 (b2 a)) = (a ∪ (ab ))

Theoremud2lem2 564 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (ab )) →2 a) = (ab)

Theoremud2lem3 565 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a2 b) →2 (ab)) = (ab)

Theoremud3lem1a 566 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∩ (b3 a)) = (ab )

Theoremud3lem1b 567 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∩ (b3 a) ) = 0

Theoremud3lem1c 568 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∪ (b3 a)) = (ab )

Theoremud3lem1d 569 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∩ ((a3 b) ∪ (b3 a))) = ((ab ) ∪ (a ∩ (ab)))

Theoremud3lem1 570 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) →3 (b3 a)) = (a ∪ (ab ))

Theoremud3lem2 571 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (ab )) →3 a) = (ab)

Theoremud3lem3a 572 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∩ (ab)) = (a3 b)

Theoremud3lem3b 573 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∩ (ab) ) = 0

Theoremud3lem3c 574 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∪ (ab)) = (ab)

Theoremud3lem3d 575 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) ∩ ((a3 b) ∪ (ab))) = ((ab) ∪ (a ∩ (ab)))

Theoremud3lem3 576 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a3 b) →3 (ab)) = (ab)

Theoremud4lem1a 577 Lemma for unified disjunction. (Contributed by NM, 24-Nov-1997.)
((a4 b) ∩ (b4 a)) = ((ab) ∪ (ab ))

Theoremud4lem1b 578 Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
((a4 b) ∩ (b4 a)) = (ab )

Theoremud4lem1c 579 Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
((a4 b) ∪ (b4 a)) = (ab )

Theoremud4lem1d 580 Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
(((a4 b) ∪ (b4 a)) ∩ (b4 a) ) = (((ab ) ∩ (ab)) ∩ a)

Theoremud4lem1 581 Lemma for unified disjunction. (Contributed by NM, 25-Nov-1997.)
((a4 b) →4 (b4 a)) = (a ∪ (ab ))

Theoremud4lem2 582 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a ∪ (ab )) →4 a) = (ab)

Theoremud4lem3a 583 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a4 b) ∩ (ab)) = (a4 b)

Theoremud4lem3b 584 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a4 b) ∪ (ab)) = (ab)

Theoremud4lem3 585 Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
((a4 b) →4 (ab)) = (ab)

Theoremud5lem1a 586 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a5 b) ∩ (b5 a)) = ((ab) ∪ (ab ))

Theoremud5lem1b 587 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a5 b) ∩ (b5 a)) = (ab )

Theoremud5lem1c 588 Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a5 b) ∩ (b5 a) ) = (((ab) ∩ (ab )) ∩ ((ab) ∩ (ab )))

Theoremud5lem1 589 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a5 b) →5 (b5 a)) = (ab )

Theoremud5lem2 590 Lemma for unified disjunction. (Contributed by NM, 10-Apr-2012.)
((ab ) →5 a) = (a ∪ (ab))

Theoremud5lem3a 591 Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
((a5 b) ∩ (a ∪ (ab))) = ((ab) ∪ (ab))

Theoremud5lem3b 592 Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a5 b) ∩ (a ∪ (ab))) = (a ∩ (ab ))

Theoremud5lem3c 593 Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a5 b) ∩ (a ∪ (ab)) ) = (((ab) ∩ (ab )) ∩ a )

Theoremud5lem3 594 Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
((a5 b) →5 (a ∪ (ab))) = (ab)

Theoremud1 595 Unified disjunction for Sasaki implication. (Contributed by NM, 23-Nov-1997.)
(ab) = ((a1 b) →1 (((a1 b) →1 (b1 a)) →1 a))

Theoremud2 596 Unified disjunction for Dishkant implication. (Contributed by NM, 23-Nov-1997.)
(ab) = ((a2 b) →2 (((a2 b) →2 (b2 a)) →2 a))

Theoremud3 597 Unified disjunction for Kalmbach implication. (Contributed by NM, 23-Nov-1997.)
(ab) = ((a3 b) →3 (((a3 b) →3 (b3 a)) →3 a))

Theoremud4 598 Unified disjunction for non-tollens implication. (Contributed by NM, 23-Nov-1997.)
(ab) = ((a4 b) →4 (((a4 b) →4 (b4 a)) →4 a))

Theoremud5 599 Unified disjunction for relevance implication. (Contributed by NM, 23-Nov-1997.)
(ab) = ((a5 b) →5 (((a5 b) →5 (b5 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. (Contributed by NM, 14-Dec-1997.)
((a1 b) ∩ a) = (ab)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500501-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 >