Type  Label  Description 
Statement 

Theorem  sylnib 601 
A mixed syllogism inference from an implication and a biconditional.
(Contributed by Wolf Lammen, 16Dec2013.)



Theorem  sylnibr 602 
A mixed syllogism inference from an implication and a biconditional.
Useful for substituting an consequent with a definition. (Contributed
by Wolf Lammen, 16Dec2013.)



Theorem  sylnbi 603 
A mixed syllogism inference from a biconditional and an implication.
Useful for substituting an antecedent with a definition. (Contributed
by Wolf Lammen, 16Dec2013.)



Theorem  sylnbir 604 
A mixed syllogism inference from a biconditional and an implication.
(Contributed by Wolf Lammen, 16Dec2013.)



Theorem  xchnxbi 605 
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27Sep2014.)



Theorem  xchnxbir 606 
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27Sep2014.)



Theorem  xchbinx 607 
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27Sep2014.)



Theorem  xchbinxr 608 
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27Sep2014.)



Theorem  mt2bi 609 
A false consequent falsifies an antecedent. (Contributed by NM,
19Aug1993.) (Proof shortened by Wolf Lammen, 12Nov2012.)



Theorem  mtt 610 
Modustollenslike theorem. (Contributed by NM, 7Apr2001.) (Revised by
Mario Carneiro, 31Jan2015.)



Theorem  pm5.21 611 
Two propositions are equivalent if they are both false. Theorem *5.21 of
[WhiteheadRussell] p. 124.
(Contributed by NM, 21May1994.) (Revised by
Mario Carneiro, 31Jan2015.)



Theorem  pm5.21im 612 
Two propositions are equivalent if they are both false. Closed form of
2false 617. Equivalent to a bi2 121like version of the xorconnective.
(Contributed by Wolf Lammen, 13May2013.) (Revised by Mario Carneiro,
31Jan2015.)



Theorem  nbn2 613 
The negation of a wff is equivalent to the wff's equivalence to falsehood.
(Contributed by Juha Arpiainen, 19Jan2006.) (Revised by Mario Carneiro,
31Jan2015.)



Theorem  bibif 614 
Transfer negation via an equivalence. (Contributed by NM, 3Oct2007.)
(Proof shortened by Wolf Lammen, 28Jan2013.)



Theorem  nbn 615 
The negation of a wff is equivalent to the wff's equivalence to
falsehood. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf
Lammen, 3Oct2013.)



Theorem  nbn3 616 
Transfer falsehood via equivalence. (Contributed by NM,
11Sep2006.)



Theorem  2false 617 
Two falsehoods are equivalent. (Contributed by NM, 4Apr2005.)
(Revised by Mario Carneiro, 31Jan2015.)



Theorem  2falsed 618 
Two falsehoods are equivalent (deduction rule). (Contributed by NM,
11Oct2013.)



Theorem  pm5.21ni 619 
Two propositions implying a false one are equivalent. (Contributed by
NM, 16Feb1996.) (Proof shortened by Wolf Lammen, 19May2013.)



Theorem  pm5.21nii 620 
Eliminate an antecedent implied by each side of a biconditional.
(Contributed by NM, 21May1999.) (Revised by Mario Carneiro,
31Jan2015.)



Theorem  pm5.21ndd 621 
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 622 
Theorem *5.19 of [WhiteheadRussell] p.
124. (Contributed by NM,
3Jan2005.) (Revised by Mario Carneiro, 31Jan2015.)



Theorem  pm4.8 623 
Theorem *4.8 of [WhiteheadRussell] p.
122. This one holds for all
propositions, but compare with pm4.81dc 814 which requires a decidability
condition. (Contributed by NM, 3Jan2005.)



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



Theorem  imnani 625 
Express implication in terms of conjunction. (Contributed by Mario
Carneiro, 28Sep2015.)



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



Theorem  pm3.24 627 
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.)



Theorem  notnotnot 628 
Triple negation. (Contributed by Jim Kingdon, 28Jul2018.)



1.2.6 Logical disjunction


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



Axiom  axio 630 
Definition of 'or'. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31Jan2015.)



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



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



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



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



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



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



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



Theorem  mpjaod 638 
Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro,
29May2016.)



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



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



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



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



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



Theorem  orel1 644 
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 645 
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 646 
Axiom *1.4 of [WhiteheadRussell] p.
96. (Contributed by NM, 3Jan2005.)
(Revised by NM, 15Nov2012.)



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



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



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



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



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



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



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



Theorem  orcs 654 
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 14)
type inference
in a proof. (Contributed by NM, 21Jun1994.)



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



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



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



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



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



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



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



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



Theorem  biorf 663 
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 664 
A wff is equivalent to its negated disjunction with falsehood.
(Contributed by NM, 9Jul2012.)



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



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



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



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



Theorem  ioran 669 
Negated disjunction in terms of conjunction. This version of DeMorgan's
law is a biconditional for all propositions (not just decidable ones),
unlike oranim 807, anordc 863, or ianordc 799. Compare Theorem *4.56 of
[WhiteheadRussell] p. 120.
(Contributed by NM, 5Aug1993.) (Revised by
Mario Carneiro, 31Jan2015.)



Theorem  pm3.14 670 
Theorem *3.14 of [WhiteheadRussell] p.
111. One direction of De Morgan's
law). The biconditional holds for decidable propositions as seen at
ianordc 799. The converse holds for decidable
propositions, as seen at
pm3.13dc 866. (Contributed by NM, 3Jan2005.) (Revised
by Mario
Carneiro, 31Jan2015.)



Theorem  pm3.1 671 
Theorem *3.1 of [WhiteheadRussell] p.
111. The converse holds for
decidable propositions, as seen at anordc 863. (Contributed by NM,
3Jan2005.) (Revised by Mario Carneiro, 31Jan2015.)



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



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



Theorem  oridm 674 
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 675 
Theorem *4.25 of [WhiteheadRussell] p.
117. (Contributed by NM,
3Jan2005.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

