Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  jca 518 
Deduce conjunction of the consequents of two implications ("join
consequents with 'and'"). Equivalent to the natural deduction rule
I ( introduction), see
natded in set.mm. (Contributed by
NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 25Oct2012.)



Theorem  jcad 519 
Deduction conjoining the consequents of two implications. (Contributed
by NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 23Jul2013.)



Theorem  jca31 520 
Join three consequents. (Contributed by Jeff Hankins, 1Aug2009.)



Theorem  jca32 521 
Join three consequents. (Contributed by FL, 1Aug2009.)



Theorem  jcai 522 
Deduction replacing implication with conjunction. (Contributed by NM,
5Aug1993.)



Theorem  jctil 523 
Inference conjoining a theorem to left of consequent in an implication.
(Contributed by NM, 31Dec1993.)



Theorem  jctir 524 
Inference conjoining a theorem to right of consequent in an
implication. (Contributed by NM, 31Dec1993.)



Theorem  jctl 525 
Inference conjoining a theorem to the left of a consequent.
(Contributed by NM, 31Dec1993.) (Proof shortened by Wolf Lammen,
24Oct2012.)



Theorem  jctr 526 
Inference conjoining a theorem to the right of a consequent.
(Contributed by NM, 18Aug1993.) (Proof shortened by Wolf Lammen,
24Oct2012.)



Theorem  jctild 527 
Deduction conjoining a theorem to left of consequent in an implication.
(Contributed by NM, 21Apr2005.)



Theorem  jctird 528 
Deduction conjoining a theorem to right of consequent in an
implication. (Contributed by NM, 21Apr2005.)



Theorem  ancl 529 
Conjoin antecedent to left of consequent. (Contributed by NM,
15Aug1994.)



Theorem  anclb 530 
Conjoin antecedent to left of consequent. Theorem *4.7 of
[WhiteheadRussell] p. 120.
(Contributed by NM, 25Jul1999.) (Proof
shortened by Wolf Lammen, 24Mar2013.)



Theorem  pm5.42 531 
Theorem *5.42 of [WhiteheadRussell] p.
125. (Contributed by NM,
3Jan2005.)



Theorem  ancr 532 
Conjoin antecedent to right of consequent. (Contributed by NM,
15Aug1994.)



Theorem  ancrb 533 
Conjoin antecedent to right of consequent. (Contributed by NM,
25Jul1999.) (Proof shortened by Wolf Lammen, 24Mar2013.)



Theorem  ancli 534 
Deduction conjoining antecedent to left of consequent. (Contributed by
NM, 12Aug1993.)



Theorem  ancri 535 
Deduction conjoining antecedent to right of consequent. (Contributed by
NM, 15Aug1994.)



Theorem  ancld 536 
Deduction conjoining antecedent to left of consequent in nested
implication. (Contributed by NM, 15Aug1994.) (Proof shortened by
Wolf Lammen, 1Nov2012.)



Theorem  ancrd 537 
Deduction conjoining antecedent to right of consequent in nested
implication. (Contributed by NM, 15Aug1994.) (Proof shortened by
Wolf Lammen, 1Nov2012.)



Theorem  anc2l 538 
Conjoin antecedent to left of consequent in nested implication.
(Contributed by NM, 10Aug1994.) (Proof shortened by Wolf Lammen,
14Jul2013.)



Theorem  anc2r 539 
Conjoin antecedent to right of consequent in nested implication.
(Contributed by NM, 15Aug1994.)



Theorem  anc2li 540 
Deduction conjoining antecedent to left of consequent in nested
implication. (Contributed by NM, 10Aug1994.) (Proof shortened by
Wolf Lammen, 7Dec2012.)



Theorem  anc2ri 541 
Deduction conjoining antecedent to right of consequent in nested
implication. (Contributed by NM, 15Aug1994.) (Proof shortened by
Wolf Lammen, 7Dec2012.)



Theorem  pm3.41 542 
Theorem *3.41 of [WhiteheadRussell] p.
113. (Contributed by NM,
3Jan2005.)



Theorem  pm3.42 543 
Theorem *3.42 of [WhiteheadRussell] p.
113. (Contributed by NM,
3Jan2005.)



Theorem  pm3.4 544 
Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell]
p. 113. (Contributed by NM, 31Jul1995.)



Theorem  pm4.45im 545 
Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell]
p. 119. (Contributed by NM, 17May1998.)



Theorem  anim12d 546 
Conjoin antecedents and consequents in a deduction. (Contributed by NM,
3Apr1994.) (Proof shortened by Wolf Lammen, 18Dec2013.)



Theorem  anim1d 547 
Add a conjunct to right of antecedent and consequent in a deduction.
(Contributed by NM, 3Apr1994.)



Theorem  anim2d 548 
Add a conjunct to left of antecedent and consequent in a deduction.
(Contributed by NM, 5Aug1993.)



Theorem  anim12i 549 
Conjoin antecedents and consequents of two premises. (Contributed by
NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 14Dec2013.)



Theorem  anim12ci 550 
Variant of anim12i 549 with commutation. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  anim1i 551 
Introduce conjunct to both sides of an implication. (Contributed by NM,
5Aug1993.)



Theorem  anim2i 552 
Introduce conjunct to both sides of an implication. (Contributed by NM,
5Aug1993.)



Theorem  anim12ii 553 
Conjoin antecedents and consequents in a deduction. (Contributed by NM,
11Nov2007.) (Proof shortened by Wolf Lammen, 19Jul2013.)



Theorem  prth 554 
Conjoin antecedents and consequents of two premises. This is the closed
theorem form of anim12d 546. Theorem *3.47 of [WhiteheadRussell] p. 113.
It was proved by Leibniz, and it evidently pleased him enough to call it
praeclarum theorema (splendid theorem). (Contributed by NM,
12Aug1993.) (Proof shortened by Wolf Lammen, 7Apr2013.)



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



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



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



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



Theorem  pm2.65da 559 
Deduction rule for proof by contradiction. (Contributed by NM,
12Jun2014.)



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



Theorem  pm4.14 561 
Theorem *4.14 of [WhiteheadRussell] p.
117. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 23Oct2012.)



Theorem  pm3.37 562 
Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 23Oct2012.)



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



Theorem  pm4.15 564 
Theorem *4.15 of [WhiteheadRussell] p.
117. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 18Nov2012.)



Theorem  pm4.78 565 
Theorem *4.78 of [WhiteheadRussell] p.
121. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 19Nov2012.)



Theorem  pm4.79 566 
Theorem *4.79 of [WhiteheadRussell] p.
121. (Contributed by NM,
3Jan2005.) (Proof shortened by Wolf Lammen, 27Jun2013.)



Theorem  pm4.87 567 
Theorem *4.87 of [WhiteheadRussell] p.
122. (Contributed by NM,
3Jan2005.) (Proof shortened by Eric Schmidt, 26Oct2006.)



Theorem  pm3.33 568 
Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3Jan2005.)



Theorem  pm3.34 569 
Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3Jan2005.)



Theorem  pm3.35 570 
Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112.
(Contributed by NM, 14Dec2002.)



Theorem  pm5.31 571 
Theorem *5.31 of [WhiteheadRussell] p.
125. (Contributed by NM,
3Jan2005.)



Theorem  imp4a 572 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp4b 573 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp4c 574 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp4d 575 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp41 576 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp42 577 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp43 578 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp44 579 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp45 580 
An importation inference. (Contributed by NM, 26Apr1994.)



Theorem  imp5a 581 
An importation inference. (Contributed by Jeff Hankins, 7Jul2009.)



Theorem  imp5d 582 
An importation inference. (Contributed by Jeff Hankins, 7Jul2009.)



Theorem  imp5g 583 
An importation inference. (Contributed by Jeff Hankins, 7Jul2009.)



Theorem  imp55 584 
An importation inference. (Contributed by Jeff Hankins, 7Jul2009.)



Theorem  imp511 585 
An importation inference. (Contributed by Jeff Hankins, 7Jul2009.)



Theorem  expimpd 586 
Exportation followed by a deduction version of importation.
(Contributed by NM, 6Sep2008.)



Theorem  exp31 587 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp32 588 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp4a 589 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp4b 590 
An exportation inference. (Contributed by NM, 26Apr1994.) (Proof
shortened by Wolf Lammen, 23Nov2012.)



Theorem  exp4c 591 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp4d 592 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp41 593 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp42 594 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp43 595 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp44 596 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  exp45 597 
An exportation inference. (Contributed by NM, 26Apr1994.)



Theorem  expr 598 
Export a wff from a right conjunct. (Contributed by Jeff Hankins,
30Aug2009.)



Theorem  exp5c 599 
An exportation inference. (Contributed by Jeff Hankins, 7Jul2009.)



Theorem  exp53 600 
An exportation inference. (Contributed by Jeff Hankins,
30Aug2009.)

