Quantum Logic Explorer - mmtheorems6

Jump to page: 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-1024

Statement List for Quantum Logic Explorer - 501-600 - Page 6 of 11

Type	Label	Description
Statement
Theorem	binr3 501	Pavicic binary logic axr3 analog.
(a ->3 c) = 1   &   (b ->3 c) = 1   =>   ((a v b) ->3 c) = 1
Theorem	i31 502	Theorem for Kalmbach implication.
(a ->3 1) = 1
Theorem	i3aa 503	Add antecedent.
a = 1   =>   (b ->3 a) = 1
Theorem	i3abs1 504	Antecedent absorption.
(a ->3 (a ->3 (a ->3 b))) = (a ->3 (a ->3 b))
Theorem	i3abs2 505	Antecedent absorption.
(a ->3 (a ->3 (a ->3 b))) = 1   =>   (a ->3 (a ->3 b)) = 1
Theorem	i3abs3 506	Antecedent absorption.
((a ->3 b) ->3 ((a ->3 b) ->3 a)) = ((a ->3 b) ->3 a)
Theorem	i3orcom 507	Commutative law for conjunction with Kalmbach implication.
((a v b) ->3 (b v a)) = 1
Theorem	i3ancom 508	Commutative law for disjunction with Kalmbach implication.
((a ^ b) ->3 (b ^ a)) = 1
Theorem	bi3tr 509	Transitive inference.
a = b   &   (b ->3 c) = 1   =>   (a ->3 c) = 1
Theorem	i3btr 510	Transitive inference.
(a ->3 b) = 1   &   b = c   =>   (a ->3 c) = 1
Theorem	i33tr1 511	Transitive inference useful for introducing definitions.
(a ->3 b) = 1   &   c = a   &   d = b   =>   (c ->3 d) = 1
Theorem	i33tr2 512	Transitive inference useful for eliminating definitions.
(a ->3 b) = 1   &   a = c   &   b = d   =>   (c ->3 d) = 1
Theorem	i3con1 513	Contrapositive.
(a_|_ ->3 b_|_) = 1   =>   (b ->3 a) = 1
Theorem	i3ror 514	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((a v c) ->3 (b v c)) = 1
Theorem	i3lor 515	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((c v a) ->3 (c v b)) = 1
Theorem	i32or 516	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (c ->3 d) = 1   =>   ((a v c) ->3 (b v d)) = 1
Theorem	i3ran 517	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((a ^ c) ->3 (b ^ c)) = 1
Theorem	i3lan 518	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((c ^ a) ->3 (c ^ b)) = 1
Theorem	i32an 519	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (c ->3 d) = 1   =>   ((a ^ c) ->3 (b ^ d)) = 1
Theorem	i3ri3 520	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (b ->3 a) = 1   =>   ((a ->3 c) ->3 (b ->3 c)) = 1
Theorem	i3li3 521	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (b ->3 a) = 1   =>   ((c ->3 a) ->3 (c ->3 b)) = 1
Theorem	i32i3 522	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
Theorem	i0i3tr 523	Transitive inference.
(a ->3 (a ->3 b)) = 1   &   (b ->3 c) = 1   =>   (a ->3 (a ->3 c)) = 1
Theorem	i3i0tr 524	Transitive inference.
(a ->3 b) = 1   &   (b ->3 (b ->3 c)) = 1   =>   (a ->3 (a ->3 c)) = 1
Theorem	i3th1 525	Theorem for Kalmbach implication.
(a ->3 (a ->3 (b ->3 a))) = 1
Theorem	i3th2 526	Theorem for Kalmbach implication.
(a ->3 (b ->3 (b ->3 a))) = 1
Theorem	i3th3 527	Theorem for Kalmbach implication.
(a_|_ ->3 (a ->3 (a ->3 b))) = 1
Theorem	i3th4 528	Theorem for Kalmbach implication.
(a ->3 (b ->3 b)) = 1
Theorem	i3th5 529	Theorem for Kalmbach implication.
((a ->3 b) ->3 (a ->3 (a ->3 b))) = 1
Theorem	i3th6 530	Theorem for Kalmbach implication.
((a ->3 (a ->3 (a ->3 b))) ->3 (a ->3 (a ->3 b))) = 1
Theorem	i3th7 531	Theorem for Kalmbach implication.
(a ->3 ((a ->3 b) ->3 a)) = 1
Theorem	i3th8 532	Theorem for Kalmbach implication.
((a ->3 b)_|_ ->3 ((a ->3 b) ->3 a)) = 1
Theorem	i3con 533	Theorem for Kalmbach implication.
((a ->3 b) ->3 ((a ->3 b) ->3 (b_|_ ->3 a_|_))) = 1
Theorem	i3orlem1 534	Lemma for Kalmbach implication OR builder.
((a v c) ^ ((a v c)_|_ v (b v c))) =< ((a v c) ->3 (b v c))
Theorem	i3orlem2 535	Lemma for Kalmbach implication OR builder.
(a ^ b) =< ((a v c) ->3 (b v c))
Theorem	i3orlem3 536	Lemma for Kalmbach implication OR builder.
c =< ((a v c) ->3 (b v c))
Theorem	i3orlem4 537	Lemma for Kalmbach implication OR builder.
((a v c)_|_ ^ (b v c)) =< ((a v c) ->3 (b v c))
Theorem	i3orlem5 538	Lemma for Kalmbach implication OR builder.
((a_|_ ^ b_|_) ^ c_|_) =< ((a v c) ->3 (b v c))
Theorem	i3orlem6 539	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)))
Theorem	i3orlem7 540	Lemma for Kalmbach implication OR builder.
(a ^ b_|_) =< ((a ->3 b)_|_ v ((a v c) ->3 (b v c)))
Theorem	i3orlem8 541	Lemma for Kalmbach implication OR builder.
(((a v b) ^ (a v b_|_)) ^ a_|_) =< ((a ->3 b)_|_ v ((a v c) ->3 (b v c)))
Theorem	ud1lem1 542	Lemma for unified disjunction.
((a ->1 b) ->1 (b ->1 a)) = (a v (a_|_ ^ b_|_))
Theorem	ud1lem2 543	Lemma for unified disjunction.
((a v (a_|_ ^ b_|_)) ->1 a) = (a v b)
Theorem	ud1lem3 544	Lemma for unified disjunction.
((a ->1 b) ->1 (a v b)) = (a v b)
Theorem	ud2lem1 545	Lemma for unified disjunction.
((a ->2 b) ->2 (b ->2 a)) = (a v (a_|_ ^ b_|_))
Theorem	ud2lem2 546	Lemma for unified disjunction.
((a v (a_|_ ^ b_|_)) ->2 a) = (a v b)
Theorem	ud2lem3 547	Lemma for unified disjunction.
((a ->2 b) ->2 (a v b)) = (a v b)
Theorem	ud3lem1a 548	Lemma for unified disjunction.
((a ->3 b)_|_ ^ (b ->3 a)) = (a ^ b_|_)
Theorem	ud3lem1b 549	Lemma for unified disjunction.
((a ->3 b)_|_ ^ (b ->3 a)_|_) = 0
Theorem	ud3lem1c 550	Lemma for unified disjunction.
((a ->3 b)_|_ v (b ->3 a)) = (a v b_|_)
Theorem	ud3lem1d 551	Lemma for unified disjunction.
((a ->3 b) ^ ((a ->3 b)_|_ v (b ->3 a))) = ((a_|_ ^ b_|_) v (a ^ (a_|_ v b)))
Theorem	ud3lem1 552	Lemma for unified disjunction.
((a ->3 b) ->3 (b ->3 a)) = (a v (a_|_ ^ b_|_))
Theorem	ud3lem2 553	Lemma for unified disjunction.
((a v (a_|_ ^ b_|_)) ->3 a) = (a v b)
Theorem	ud3lem3a 554	Lemma for unified disjunction.
((a ->3 b)_|_ ^ (a v b)) = (a ->3 b)_|_
Theorem	ud3lem3b 555	Lemma for unified disjunction.
((a ->3 b)_|_ ^ (a v b)_|_) = 0
Theorem	ud3lem3c 556	Lemma for unified disjunction.
((a ->3 b)_|_ v (a v b)) = (a v b)
Theorem	ud3lem3d 557	Lemma for unified disjunction.
((a ->3 b) ^ ((a ->3 b)_|_ v (a v b))) = ((a_|_ ^ b) v (a ^ (a_|_ v b)))
Theorem	ud3lem3 558	Lemma for unified disjunction.
((a ->3 b) ->3 (a v b)) = (a v b)
Theorem	ud4lem1a 559	Lemma for unified disjunction.
((a ->4 b) ^ (b ->4 a)) = ((a ^ b) v (a_|_ ^ b_|_))
Theorem	ud4lem1b 560	Lemma for unified disjunction.
((a ->4 b)_|_ ^ (b ->4 a)) = (a ^ b_|_)
Theorem	ud4lem1c 561	Lemma for unified disjunction.
((a ->4 b)_|_ v (b ->4 a)) = (a v b_|_)
Theorem	ud4lem1d 562	Lemma for unified disjunction.
(((a ->4 b)_|_ v (b ->4 a)) ^ (b ->4 a)_|_) = (((a_|_ v b_|_) ^ (a_|_ v b)) ^ a)
Theorem	ud4lem1 563	Lemma for unified disjunction.
((a ->4 b) ->4 (b ->4 a)) = (a v (a_|_ ^ b_|_))
Theorem	ud4lem2 564	Lemma for unified disjunction.
((a v (a_|_ ^ b_|_)) ->4 a) = (a v b)
Theorem	ud4lem3a 565	Lemma for unified disjunction.
((a ->4 b)_|_ ^ (a v b)) = (a ->4 b)_|_
Theorem	ud4lem3b 566	Lemma for unified disjunction.
((a ->4 b)_|_ v (a v b)) = (a v b)
Theorem	ud4lem3 567	Lemma for unified disjunction.
((a ->4 b) ->4 (a v b)) = (a v b)
Theorem	ud5lem1a 568	Lemma for unified disjunction.
((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a_|_ ^ b_|_))
Theorem	ud5lem1b 569	Lemma for unified disjunction.
((a ->5 b)_|_ ^ (b ->5 a)) = (a ^ b_|_)
Theorem	ud5lem1c 570	Lemma for unified disjunction.
((a ->5 b)_|_ ^ (b ->5 a)_|_) = (((a v b) ^ (a v b_|_)) ^ ((a_|_ v b) ^ (a_|_ v b_|_)))
Theorem	ud5lem1 571	Lemma for unified disjunction.
((a ->5 b) ->5 (b ->5 a)) = (a v b_|_)
Theorem	ud5lem2 572	Lemma for unified disjunction.
((a v b_|_) ->5 a) = (a v (a_|_ ^ b))
Theorem	ud5lem3a 573	Lemma for unified disjunction.
((a ->5 b) ^ (a v (a_|_ ^ b))) = ((a ^ b) v (a_|_ ^ b))
Theorem	ud5lem3b 574	Lemma for unified disjunction.
((a ->5 b)_|_