Type  Label  Description 
Statement 

Theorem  pm5.21ndd 601 
Eliminate an antecedent implied by each side of a biconditional,
deduction version. (Contributed by Paul Chapman, 21Nov2012.)
(Revised by Mario Carneiro, 31Jan2015.)



Theorem  pm5.19 602 
Theorem *5.19 of [WhiteheadRussell] p.
124. (Contributed by NM,
3Jan2005.) (Revised by Mario Carneiro, 31Jan2015.)



Theorem  pm4.8 603 
Theorem *4.8 of [WhiteheadRussell] p.
122. This one is valid in
intuitionistic logic, whereas pm4.81 2074 is not. (Contributed by NM,
3Jan2005.)



Theorem  imnan 604 
Express implication in terms of conjunction. (Contributed by NM,
9Apr1994.) (Revised by Mario Carneiro, 1Feb2015.)



Theorem  nan 605 
Theorem to move a conjunct in and out of a negation. (Contributed by NM,
9Nov2003.)



Theorem  pm3.24 606 
Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who
call it the "law of contradiction"). (Contributed by NM,
16Sep1993.)
(Revised by Mario Carneiro, 2Feb2015.)



1.2.6 Logical disjunction


Syntax  wo 607 
Extend wff definition to include disjunction ('or').



Axiom  axio 608 
Definition of 'or'. Axiom 6 of 10 for intuitionistic logic. (Contributed
by Mario Carneiro, 31Jan2015.)



Theorem  jaob 609 
Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell]
p. 121. (Contributed by NM, 30May1994.) (Revised by Mario Carneiro,
31Jan2015.)



Theorem  olc 610 
Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96.
(Contributed by NM, 30Aug1993.) (Revised by NM, 31Jan2015.)



Theorem  orc 611 
Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104.
(Contributed by NM, 30Aug1993.) (Revised by NM, 31Jan2015.)



Theorem  pm2.672 612 
Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107.
(Contributed by NM, 3Jan2005.) (Revised by NM, 9Dec2012.)



Theorem  pm3.44 613 
Theorem *3.44 of [WhiteheadRussell] p.
113. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 3Oct2013.)



Theorem  jaoi 614 
Inference disjoining the antecedents of two implications. (Contributed
by NM, 5Apr1994.) (Revised by NM, 31Jan2015.)



Theorem  jaod 615 
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 18Aug1994.) (Revised by NM, 4Apr2013.)



Theorem  jaao 616 
Inference conjoining and disjoining the antecedents of two
implications. (Contributed by NM, 30Sep1999.)



Theorem  jaoa 617 
Inference disjoining and conjoining the antecedents of two
implications. (Contributed by Stefan Allan, 1Nov2008.)



Theorem  pm2.53 618 
Theorem *2.53 of [WhiteheadRussell] p.
107. This holds
intuitionistically, although its converse, pm2.54 1972, does not.
(Contributed by NM, 3Jan2005.) (Revised by NM, 31Jan2015.)



Theorem  ori 619 
Infer implication from disjunction. (Contributed by NM, 11Jun1994.)
(Revised by Mario Carneiro, 31Jan2015.)



Theorem  ord 620 
Deduce implication from disjunction. (Contributed by NM, 18May1994.)
(Revised by Mario Carneiro, 31Jan2015.)



Theorem  orel1 621 
Elimination of disjunction by denial of a disjunct. Theorem *2.55 of
[WhiteheadRussell] p. 107.
(Contributed by NM, 12Aug1994.) (Proof
shortened by Wolf Lammen, 21Jul2012.)



Theorem  orel2 622 
Elimination of disjunction by denial of a disjunct. Theorem *2.56 of
[WhiteheadRussell] p. 107.
(Contributed by NM, 12Aug1994.) (Proof
shortened by Wolf Lammen, 5Apr2013.)



Theorem  pm1.4 623 
Axiom *1.4 of [WhiteheadRussell] p.
96. (Contributed by NM, 3Jan2005.)
(Revised by NM, 15Nov2012.)



Theorem  orcom 624 
Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell]
p. 118. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf
Lammen, 15Nov2012.)



Theorem  orcomd 625 
Commutation of disjuncts in consequent. (Contributed by NM,
2Dec2010.)



Theorem  orcoms 626 
Commutation of disjuncts in antecedent. (Contributed by NM,
2Dec2012.)



Theorem  orci 627 
Deduction introducing a disjunct. (Contributed by NM, 19Jan2008.)
(Revised by Mario Carneiro, 31Jan2015.)



Theorem  olci 628 
Deduction introducing a disjunct. (Contributed by NM, 19Jan2008.)
(Revised by Mario Carneiro, 31Jan2015.)



Theorem  orcd 629 
Deduction introducing a disjunct. (Contributed by NM, 20Sep2007.)



Theorem  olcd 630 
Deduction introducing a disjunct. (Contributed by NM, 11Apr2008.)
(Proof shortened by Wolf Lammen, 3Oct2013.)



Theorem  orcs 631 
Deduction eliminating disjunct. Notational convention: We sometimes
suffix with "s" the label of an inference that manipulates an
antecedent, leaving the consequent unchanged. The "s" means
that the
inference eliminates the need for a syllogism (syl 13)
type inference
in a proof. (Contributed by NM, 21Jun1994.)



Theorem  olcs 632 
Deduction eliminating disjunct. (Contributed by NM, 21Jun1994.)
(Proof shortened by Wolf Lammen, 3Oct2013.)



Theorem  pm2.07 633 
Theorem *2.07 of [WhiteheadRussell] p.
101. (Contributed by NM,
3Jan2005.)



Theorem  pm2.45 634 
Theorem *2.45 of [WhiteheadRussell] p.
106. (Contributed by NM,
3Jan2005.)



Theorem  pm2.46 635 
Theorem *2.46 of [WhiteheadRussell] p.
106. (Contributed by NM,
3Jan2005.)



Theorem  pm2.47 636 
Theorem *2.47 of [WhiteheadRussell] p.
107. (Contributed by NM,
3Jan2005.)



Theorem  pm2.48 637 
Theorem *2.48 of [WhiteheadRussell] p.
107. (Contributed by NM,
3Jan2005.)



Theorem  pm2.49 638 
Theorem *2.49 of [WhiteheadRussell] p.
107. (Contributed by NM,
3Jan2005.)



Theorem  pm2.67 639 
Theorem *2.67 of [WhiteheadRussell] p.
107. (Contributed by NM,
3Jan2005.) (Revised by NM, 9Dec2012.)



Theorem  biorf 640 
A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of
[WhiteheadRussell] p. 121.
(Contributed by NM, 23Mar1995.) (Proof
shortened by Wolf Lammen, 18Nov2012.)



Theorem  biortn 641 
A wff is equivalent to its negated disjunction with falsehood.
(Contributed by NM, 9Jul2012.)



Theorem  biorfi 642 
A wff is equivalent to its disjunction with falsehood. (Contributed by
NM, 23Mar1995.)



Theorem  pm2.621 643 
Theorem *2.621 of [WhiteheadRussell]
p. 107. (Contributed by NM,
3Jan2005.) (Revised by NM, 13Dec2013.)



Theorem  pm2.62 644 
Theorem *2.62 of [WhiteheadRussell] p.
107. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 13Dec2013.)



Theorem  imorri 645 
Infer implication from disjunction. (Contributed by Jonathan BenNaim,
3Jun2011.) (Revised by Mario Carneiro, 31Jan2015.)



Theorem  ioran 646 
Negated disjunction in terms of conjunction. This version of DeMorgan's
law holds for all propositions (not just decidable ones), unlike oran 2077,
anordc 823, or ianordc 768. Compare Theorem *4.56 of [WhiteheadRussell]
p. 120. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro,
31Jan2015.)



Theorem  pm3.14 647 
Theorem *3.14 of [WhiteheadRussell] p.
111. (Contributed by NM,
3Jan2005.) (Revised by Mario Carneiro, 31Jan2015.)



Theorem  pm3.1 648 
Theorem *3.1 of [WhiteheadRussell] p.
111. (Contributed by NM,
3Jan2005.) (Revised by Mario Carneiro, 31Jan2015.)



Theorem  jao 649 
Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell]
p. 113. (Contributed by NM, 5Apr1994.) (Proof shortened by Wolf
Lammen, 4Apr2013.)



Theorem  pm1.2 650 
Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3Jan2005.) (Revised by NM, 10Mar2013.)



Theorem  oridm 651 
Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell]
p. 117. (Contributed by NM, 5Aug1993.) (Proof shortened by Andrew
Salmon, 16Apr2011.) (Proof shortened by Wolf Lammen, 10Mar2013.)



Theorem  pm4.25 652 
Theorem *4.25 of [WhiteheadRussell] p.
117. (Contributed by NM,
3Jan2005.)



Theorem  orim12i 653 
Disjoin antecedents and consequents of two premises. (Contributed by
NM, 6Jun1994.) (Proof shortened by Wolf Lammen, 25Jul2012.)



Theorem  orim1i 654 
Introduce disjunct to both sides of an implication. (Contributed by NM,
6Jun1994.)



Theorem  orim2i 655 
Introduce disjunct to both sides of an implication. (Contributed by NM,
6Jun1994.)



Theorem  orbi2i 656 
Inference adding a left disjunct to both sides of a logical
equivalence. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf
Lammen, 12Dec2012.)



Theorem  orbi1i 657 
Inference adding a right disjunct to both sides of a logical
equivalence. (Contributed by NM, 5Aug1993.)



Theorem  orbi12i 658 
Infer the disjunction of two equivalences. (Contributed by NM,
5Aug1993.)



Theorem  pm1.5 659 
Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3Jan2005.)



Theorem  or12 660 
Swap two disjuncts. (Contributed by NM, 5Aug1993.) (Proof shortened by
Wolf Lammen, 14Nov2012.)



Theorem  orass 661 
Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell]
p. 118. (Contributed by NM, 5Aug1993.) (Proof shortened by Andrew
Salmon, 26Jun2011.)



Theorem  pm2.31 662 
Theorem *2.31 of [WhiteheadRussell] p.
104. (Contributed by NM,
3Jan2005.)



Theorem  pm2.32 663 
Theorem *2.32 of [WhiteheadRussell] p.
105. (Contributed by NM,
3Jan2005.)



Theorem  or32 664 
A rearrangement of disjuncts. (Contributed by NM, 18Oct1995.) (Proof
shortened by Andrew Salmon, 26Jun2011.)



Theorem  or4 665 
Rearrangement of 4 disjuncts. (Contributed by NM, 12Aug1994.)



Theorem  or42 666 
Rearrangement of 4 disjuncts. (Contributed by NM, 10Jan2005.)



Theorem  orordi 667 
Distribution of disjunction over disjunction. (Contributed by NM,
25Feb1995.)



Theorem  orordir 668 
Distribution of disjunction over disjunction. (Contributed by NM,
25Feb1995.)



Theorem  pm2.3 669 
Theorem *2.3 of [WhiteheadRussell] p.
104. (Contributed by NM,
3Jan2005.)



Theorem  pm2.41 670 
Theorem *2.41 of [WhiteheadRussell] p.
106. (Contributed by NM,
3Jan2005.)



Theorem  pm2.42 671 
Theorem *2.42 of [WhiteheadRussell] p.
106. (Contributed by NM,
3Jan2005.)



Theorem  pm2.4 672 
Theorem *2.4 of [WhiteheadRussell] p.
106. (Contributed by NM,
3Jan2005.)



Theorem  pm4.44 673 
Theorem *4.44 of [WhiteheadRussell] p.
119. (Contributed by NM,
3Jan2005.)



Theorem  mtord 674 
A modus tollens deduction involving disjunction. (Contributed by Jeff
Hankins, 15Jul2009.) (Revised by Mario Carneiro, 31Jan2015.)



Theorem  pm4.45 675 
Theorem *4.45 of [WhiteheadRussell] p.
119. (Contributed by NM,
3Jan2005.)



Theorem  pm3.48 676 
Theorem *3.48 of [WhiteheadRussell] p.
114. (Contributed by NM,
28Jan1997.) (Revised by NM, 1Dec2012.)



Theorem  orim12d 677 
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
10May1994.)



Theorem  orim1d 678 
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
23Apr1995.)



Theorem  orim2d 679 
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
23Apr1995.)



Theorem  orim2 680 
Axiom *1.6 (Sum) of [WhiteheadRussell]
p. 97. (Contributed by NM,
3Jan2005.)



Theorem  orbi2d 681 
Deduction adding a left disjunct to both sides of a logical
equivalence. (Contributed by NM, 5Aug1993.) (Revised by Mario
Carneiro, 31Jan2015.)



Theorem  orbi1d 682 
Deduction adding a right disjunct to both sides of a logical
equivalence. (Contributed by NM, 5Aug1993.)



Theorem  orbi1 683 
Theorem *4.37 of [WhiteheadRussell] p.
118. (Contributed by NM,
3Jan2005.)



Theorem  orbi12d 684 
Deduction joining two equivalences to form equivalence of disjunctions.
(Contributed by NM, 5Aug1993.)



Theorem  pm5.61 685 
Theorem *5.61 of [WhiteheadRussell] p.
125. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 30Jun2013.)



Theorem  jaoian 686 
Inference disjoining the antecedents of two implications. (Contributed
by NM, 23Oct2005.)



Theorem  jaodan 687 
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 14Oct2005.)



Theorem  pm4.77 688 
Theorem *4.77 of [WhiteheadRussell] p.
121. (Contributed by NM,
3Jan2005.)



Theorem  pm2.63 689 
Theorem *2.63 of [WhiteheadRussell] p.
107. (Contributed by NM,
3Jan2005.)



Theorem  pm2.64 690 
Theorem *2.64 of [WhiteheadRussell] p.
107. (Contributed by NM,
3Jan2005.)



Theorem  pm5.53 691 
Theorem *5.53 of [WhiteheadRussell] p.
125. (Contributed by NM,
3Jan2005.)



Theorem  pm2.38 692 
Theorem *2.38 of [WhiteheadRussell] p.
105. (Contributed by NM,
6Mar2008.)



Theorem  pm2.36 693 
Theorem *2.36 of [WhiteheadRussell] p.
105. (Contributed by NM,
6Mar2008.)



Theorem  pm2.37 694 
Theorem *2.37 of [WhiteheadRussell] p.
105. (Contributed by NM,
6Mar2008.)



Theorem  pm2.73 695 
Theorem *2.73 of [WhiteheadRussell] p.
108. (Contributed by NM,
3Jan2005.)



Theorem  pm2.74 696 
Theorem *2.74 of [WhiteheadRussell] p.
108. (Contributed by NM,
3Jan2005.) (Proof shortened by Mario Carneiro, 31Jan2015.)



Theorem  pm2.76 697 
Theorem *2.76 of [WhiteheadRussell] p.
108. (Contributed by NM,
3Jan2005.) (Revised by Mario Carneiro, 31Jan2015.)



Theorem  pm2.75 698 
Theorem *2.75 of [WhiteheadRussell] p.
108. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 4Jan2013.)



Theorem  pm2.8 699 
Theorem *2.8 of [WhiteheadRussell] p.
108. (Contributed by NM,
3Jan2005.) (Proof shortened by Mario Carneiro, 31Jan2015.)



Theorem  pm2.81 700 
Theorem *2.81 of [WhiteheadRussell] p.
108. (Contributed by NM,
3Jan2005.)

