P. 1 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1-100   *Has distinct variable group(s)

Type	Label	Description
Statement
PART 1  INTUITIONISTIC FIRST-ORDER LOGIC WITH EQUALITY Logic can be defined as the "study of the principles of correct reasoning" (Merrilee H. Salmon's 1991 "Informal Reasoning and Informal Logic" in Informal Reasoning and Education ) or as "a formal system using symbolic techniques and mathematical methods to establish truth-values" (the Oxford English Dictionary). This section formally defines the logic system we will use. In particular, it defines symbols for declaring truthful statements, along with rules for deriving truthful statements from other truthful statements. The system defined here is intuitionistic first-order logic with equality. We begin with a few housekeeping items in pre-logic, and then introduce propositional calculus (both its axioms and important theorems that can be derived from them). Propositional calculus deals with general truths about well-formed formulas (wffs) regardless of how they are constructed. This is followed by proofs that other axiomatizations of classical propositional calculus can be derived from the axioms we have chosen to use. We then define predicate calculus, which adds additional symbols and rules useful for discussing objects (beyond simply true or false). In particular, it introduces the symbols = ("equals"), e. ("is a member of"), and A. ("for all"). The first two are called "predicates". A predicate specifies a true or false relationship between its two arguments.
1.1  Pre-logic This section includes a few "housekeeping" mechanisms before we begin defining the basics of logic.
1.1.1  Inferences for assisting proof development The inference rules in this section will normally never appear in a completed proof. They can be ignored if you are using this database to assist learning logic - please start with the statement wn 3 instead.
Theorem	idi 1	(Note: This inference rule and the next one, a1ii 2, will normally never appear in a completed proof. They can be ignored if you are using this database to assist learning logic; please start with the statement wn 3 instead.) This inference says "if ph is true then ph is true". This inference requires no axioms for its proof, and is useful as a copy-paste mechanism during proof development in mmj2. It is normally not referenced in the final version of a proof, since it is always redundant. You can remove this using the metamath-exe (Metamath program) Proof Assistant using the "MM-PA> MINIMIZE_WITH *" command. This is the inference associated with id 19, hence its name. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   =>    |- ph
Theorem	a1ii 2	(Note: This inference rule and the previous one, idi 1, will normally never appear in a completed proof.) This is a technical inference to assist proof development. It provides a temporary way to add an independent subproof to a proof under development, for later assignment to a normal proof step. The Metamath (Metamath-exe) program Proof Assistant requires proofs to be developed backwards from the conclusion with no gaps, and it has no mechanism that lets the user work on isolated subproofs. This inference provides a workaround for this limitation. It can be inserted at any point in a proof to allow an independent subproof to be developed on the side, for later use as part of the final proof. Instructions: (1) Assign this inference to any unknown step in the proof. Typically, the last unknown step is the most convenient, since "MM-PA> ASSIGN LAST" can be used. This step will be replicated in hypothesis a1ii.1, from where the development of the main proof can continue. (2) Develop the independent subproof backwards from hypothesis a1ii.2. If desired, use a "MM-PA> LET STEP" command to pre-assign the conclusion of the independent subproof to a1ii.2. (3) After the independent subproof is complete, use "MM-PA> IMPROVE ALL" to assign it automatically to an unknown step in the main proof that matches it. (4) After the entire proof is complete, use "MM-PA> MINIMIZE_WITH *" to clean up (discard) all a1ii 2 references automatically. This inference was originally designed to assist importing partially completed Proof Worksheets from the mmj2 Proof Assistant GUI, but it can also be useful on its own. Interestingly, no axioms are required for its proof. It is the inference associated with a1i 9. (Contributed by NM, 7-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   =>    |- ph
1.2  Propositional calculus Propositional calculus deals with general truths about well-formed formulas (wffs) regardless of how they are constructed. The simplest propositional truth is ( ph -> ph ), which can be read "if something is true, then it is true" - rather trivial and obvious, but nonetheless it must be proved from the axioms (see Theorem id 19). Our system of propositional calculus consists of a few basic axioms and a unique rule of inference, modus ponens. The propositional calculus used here is the intuitionistic propositional calculus. All 194 axioms, definitions, and theorems for propositional calculus in Principia Mathematica (specifically *1.2 through *5.75) are axioms or formally proven. See the Bibliographic Cross-References at https://us.metamath.org/ileuni/mmbiblio.html 19 for a complete cross-reference from sources used to its formalization in the Intuitionistic Logic Explorer.
1.2.1  Recursively define primitive wffs for propositional calculus
Syntax	wn 3	If ph is a wff, so is -. ph or "not ph". Part of the recursive definition of a wff (well-formed formula). Traditionally, Greek letters are used to represent wffs, and we follow this convention. In propositional calculus, we define only wffs built up from other wffs, i.e., there is no starting or "atomic" wff. Later, in predicate calculus, we will extend the basic wff definition by including atomic wffs (weq 1496 and wel 2142).
wff -. ph
Syntax	wi 4	If ph and ps are wff's, so is ( ph -> ps ) or " ph implies ps". Part of the recursive definition of a wff. The left-hand wff is called the antecedent, and the right-hand wff is called the consequent. In the case of ( ph -> ( ps -> ch ) ), the middle ps may be informally called either an antecedent or part of the consequent depending on context.
wff ( ph -> ps )
1.2.2  Propositional logic axioms for implication
Axiom	ax-mp 5	Rule of Modus Ponens. The postulated inference rule of propositional calculus. See, e.g., Rule 1 of [Hamilton] p. 73. The rule says, "if ph is true, and ph implies ps, then ps must also be true". This rule is sometimes called "detachment", since it detaches the minor premise from the major premise. "Modus ponens" is short for "modus ponendo ponens", a Latin phrase that means "the mode that by affirming affirms" - remark in [Sanford] p. 39. This rule is similar to the rule of modus tollens mto 657. Note: In some web page displays such as the Statement List, the symbols "& " and "=> " informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies". They are not part of the formal language. (Contributed by NM, 30-Sep-1992.)
|- ph   &    |- ( ph -> ps )   =>    |- ps
Axiom	ax-1 6	Axiom Simp. Axiom A1 of [Margaris] p. 49. One of the axioms of propositional calculus. This axiom is called Simp or "the principle of simplification" in Principia Mathematica (Theorem *2.02 of [WhiteheadRussell] p. 100) because "it enables us to pass from the joint assertion of ph and ps to the assertion of ph simply." The theorems of propositional calculus are also called tautologies. Although classical propositional logic tautologies can be proved using truth tables, there is no similarly simple system for intuitionistic propositional logic, so proving tautologies from axioms is the preferred approach. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ph ) )
Axiom	ax-2 7	Axiom Frege. Axiom A2 of [Margaris] p. 49. This axiom "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature. It is also proved as Theorem *2.77 of [WhiteheadRussell] p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 250. (Contributed by NM, 5-Aug-1993.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
1.2.3  Logical implication The results in this section are based on implication only, and only use ax-1 6, ax-2 7, and ax-mp 5. In an implication, the wff before the arrow is called the "antecedent" and the wff after the arrow is called the "consequent". We will use the following descriptive terms very loosely: A "closed form" or "tautology" has no $e hypotheses. An "inference" has one or more $e hypotheses. A "deduction" is an inference in which the hypotheses and the conclusion share the same antecedent.
Theorem	mp2b 8	A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)
|- ph   &    |- ( ph -> ps )   &    |- ( ps -> ch )   =>    |- ch
Theorem	a1i 9	Inference derived from Axiom ax-1 6. See a1d 22 for an explanation of our informal use of the terms "inference" and "deduction". See also the comment in syld 45. (Contributed by NM, 5-Aug-1993.)
|- ph   =>    |- ( ps -> ph )
Theorem	mp1i 10	Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- ph   &    |- ( ph -> ps )   =>    |- ( ch -> ps )
Theorem	a2i 11	Inference derived from Axiom ax-2 7. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph -> ps ) -> ( ph -> ch ) )
Theorem	imim2i 12	Inference adding common antecedents in an implication. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ( ch -> ph ) -> ( ch -> ps ) )
Theorem	mpd 13	A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ch )
Theorem	syl 14	An inference version of the transitive laws for implication imim2 55 and imim1 76, which Russell and Whitehead call "the principle of the syllogism...because...the syllogism in Barbara is derived from them" (quote after Theorem *2.06 of [WhiteheadRussell] p. 101). Some authors call this law a "hypothetical syllogism". (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 20-Oct-2011.) (Proof shortened by Wolf Lammen, 26-Jul-2012.)
|- ( ph -> ps )   &    |- ( ps -> ch )   =>    |- ( ph -> ch )
Theorem	mpi 15	A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
|- ps   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ch )
Theorem	mp2 16	A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
|- ph   &    |- ps   &    |- ( ph -> ( ps -> ch ) )   =>    |- ch
Theorem	3syl 17	Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   &    |- ( ps -> ch )   &    |- ( ch -> th )   =>    |- ( ph -> th )
Theorem	4syl 18	Inference chaining three syllogisms. The use of this theorem is marked "discouraged" because it can cause the "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. (Contributed by BJ, 14-Jul-2018.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ( ps -> ch )   &    |- ( ch -> th )   &    |- ( th -> ta )   =>    |- ( ph -> ta )
Theorem	id 19	Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT 20. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
|- ( ph -> ph )
Theorem	idALT 20	Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. This version is proved directly from the axioms for demonstration purposes. This proof is a popular example in the literature and is identical, step for step, to the proofs of Theorem 1 of [Margaris] p. 51, Example 2.7(a) of [Hamilton] p. 31, Lemma 10.3 of [BellMachover] p. 36, and Lemma 1.8 of [Mendelson] p. 36. It is also "Our first proof" in Hirst and Hirst's A Primer for Logic and Proof p. 17 (PDF p. 23) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf. For a shorter version of the proof that takes advantage of previously proved theorems, see id 19. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) Use id 19 instead. (New usage is discouraged.)
|- ( ph -> ph )
Theorem	idd 21	Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)
|- ( ph -> ( ps -> ps ) )
Theorem	a1d 22	Deduction introducing an embedded antecedent. (The proof was revised by Stefan Allan, 20-Mar-2006.) Naming convention: We often call a theorem a "deduction" and suffix its label with "d" whenever the hypotheses and conclusion are each prefixed with the same antecedent. This allows us to use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used; here ph would be replaced with a conjunction (wa 103) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare Theorem a1i 9. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 6. We usually show the theorem form without a suffix on its label (e.g., pm2.43 53 versus pm2.43i 49 versus pm2.43d 50). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 20-Mar-2006.)
|- ( ph -> ps )   =>    |- ( ph -> ( ch -> ps ) )
Theorem	2a1d 23	Deduction introducing two antecedents. Two applications of a1d 22. Deduction associated with 2a1 25 and 2a1i 27. (Contributed by BJ, 10-Aug-2020.)
|- ( ph -> ps )   =>    |- ( ph -> ( ch -> ( th -> ps ) ) )
Theorem	a1i13 24	Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.)
|- ( ps -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	2a1 25	A double form of ax-1 6. Its associated inference is 2a1i 27. Its associated deduction is 2a1d 23. (Contributed by BJ, 10-Aug-2020.) (Proof shortened by Wolf Lammen, 1-Sep-2020.)
|- ( ph -> ( ps -> ( ch -> ph ) ) )
Theorem	a2d 26	Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
Theorem	2a1i 27	Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
|- ch   =>    |- ( ph -> ( ps -> ch ) )
Theorem	sylcom 28	Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ps -> ( ch -> th ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	syl5com 29	Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
|- ( ph -> ps )   &    |- ( ch -> ( ps -> th ) )   =>    |- ( ph -> ( ch -> th ) )
Theorem	com12 30	Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ps -> ( ph -> ch ) )
Theorem	syl11 31	A syllogism inference. Commuted form of an instance of syl 14. (Contributed by BJ, 25-Oct-2021.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ph )   =>    |- ( ps -> ( th -> ch ) )
Theorem	syl5 32	A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)
|- ( ph -> ps )   &    |- ( ch -> ( ps -> th ) )   =>    |- ( ch -> ( ph -> th ) )
Theorem	syl6 33	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ch -> th )   =>    |- ( ph -> ( ps -> th ) )
Theorem	syl56 34	Combine syl5 32 and syl6 33. (Contributed by NM, 14-Nov-2013.)
|- ( ph -> ps )   &    |- ( ch -> ( ps -> th ) )   &    |- ( th -> ta )   =>    |- ( ch -> ( ph -> ta ) )
Theorem	syl6com 35	Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ch -> th )   =>    |- ( ps -> ( ph -> th ) )
Theorem	mpcom 36	Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.)
|- ( ps -> ph )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ps -> ch )
Theorem	syli 37	Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)
|- ( ps -> ( ph -> ch ) )   &    |- ( ch -> ( ph -> th ) )   =>    |- ( ps -> ( ph -> th ) )
Theorem	syl2im 38	Replace two antecedents. Implication-only version of syl2an 287. (Contributed by Wolf Lammen, 14-May-2013.)
|- ( ph -> ps )   &    |- ( ch -> th )   &    |- ( ps -> ( th -> ta ) )   =>    |- ( ph -> ( ch -> ta ) )
Theorem	syl2imc 39	A commuted version of syl2im 38. Implication-only version of syl2anr 288. (Contributed by BJ, 20-Oct-2021.)
|- ( ph -> ps )   &    |- ( ch -> th )   &    |- ( ps -> ( th -> ta ) )   =>    |- ( ch -> ( ph -> ta ) )
Theorem	pm2.27 40	This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 5. Theorem *2.27 of [WhiteheadRussell] p. 104. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ( ph -> ps ) -> ps ) )
Theorem	mpdd 41	A nested modus ponens deduction. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	mpid 42	A nested modus ponens deduction. (Contributed by NM, 14-Dec-2004.)
|- ( ph -> ch )   &    |- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	mpdi 43	A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by O'Cat, 15-Jan-2008.)
|- ( ps -> ch )   &    |- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	mpii 44	A doubly nested modus ponens inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 31-Jul-2012.)
|- ch   &    |- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	syld 45	Syllogism deduction. Notice that syld 45 has the same form as syl 14 with ph added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace ph with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 19 and become an antecedent. The Deduction Theorem for propositional calculus, e.g., Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ch -> th ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	syldc 46	Syllogism deduction. Commuted form of syld 45. (Contributed by BJ, 25-Oct-2021.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ch -> th ) )   =>    |- ( ps -> ( ph -> th ) )
Theorem	mp2d 47	A double modus ponens deduction. (Contributed by NM, 23-May-2013.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> th )
Theorem	a1dd 48	Deduction introducing a nested embedded antecedent. (Contributed by NM, 17-Dec-2004.) (Proof shortened by O'Cat, 15-Jan-2008.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> ( th -> ch ) ) )
Theorem	pm2.43i 49	Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
|- ( ph -> ( ph -> ps ) )   =>    |- ( ph -> ps )
Theorem	pm2.43d 50	Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
|- ( ph -> ( ps -> ( ps -> ch ) ) )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	pm2.43a 51	Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by O'Cat, 28-Nov-2008.)
|- ( ps -> ( ph -> ( ps -> ch ) ) )   =>    |- ( ps -> ( ph -> ch ) )
Theorem	pm2.43b 52	Inference absorbing redundant antecedent. (Contributed by NM, 31-Oct-1995.)
|- ( ps -> ( ph -> ( ps -> ch ) ) )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	pm2.43 53	Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. Theorem *2.43 of [WhiteheadRussell] p. 106. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 15-Aug-2004.)
|- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )
Theorem	imim2d 54	Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( th -> ps ) -> ( th -> ch ) ) )
Theorem	imim2 55	A closed form of syllogism (see syl 14). Theorem *2.05 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Sep-2012.)
|- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )
Theorem	embantd 56	Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013.)
|- ( ph -> ps )   &    |- ( ph -> ( ch -> th ) )   =>    |- ( ph -> ( ( ps -> ch ) -> th ) )
Theorem	3syld 57	Triple syllogism deduction. (Contributed by Jeff Hankins, 4-Aug-2009.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ch -> th ) )   &    |- ( ph -> ( th -> ta ) )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	sylsyld 58	A double syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
|- ( ph -> ps )   &    |- ( ph -> ( ch -> th ) )   &    |- ( ps -> ( th -> ta ) )   =>    |- ( ph -> ( ch -> ta ) )
Theorem	imim12i 59	Inference joining two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 29-Oct-2011.)
|- ( ph -> ps )   &    |- ( ch -> th )   =>    |- ( ( ps -> ch ) -> ( ph -> th ) )
Theorem	imim1i 60	Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
|- ( ph -> ps )   =>    |- ( ( ps -> ch ) -> ( ph -> ch ) )
Theorem	imim3i 61	Inference adding three nested antecedents. (Contributed by NM, 19-Dec-2006.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( th -> ph ) -> ( ( th -> ps ) -> ( th -> ch ) ) )
Theorem	sylc 62	A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ps -> ( ch -> th ) )   =>    |- ( ph -> th )
Theorem	syl3c 63	A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   =>    |- ( ph -> ta )
Theorem	syl6mpi 64	syl6 33 combined with mpi 15. (Contributed by Alan Sare, 8-Jul-2011.) (Proof shortened by Wolf Lammen, 13-Sep-2012.)
|- ( ph -> ( ps -> ch ) )   &    |- th   &    |- ( ch -> ( th -> ta ) )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	mpsyl 65	Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
|- ph   &    |- ( ps -> ch )   &    |- ( ph -> ( ch -> th ) )   =>    |- ( ps -> th )
Theorem	syl6c 66	Inference combining syl6 33 with contraction. (Contributed by Alan Sare, 2-May-2011.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ch -> ( th -> ta ) )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	syldd 67	Nested syllogism deduction. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 11-May-2013.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( ph -> ( ps -> ( th -> ta ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ta ) ) )
Theorem	syl5d 68	A nested syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by O'Cat, 2-Feb-2006.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ( ch -> ta ) ) )   =>    |- ( ph -> ( th -> ( ps -> ta ) ) )
Theorem	syl7 69	A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
|- ( ph -> ps )   &    |- ( ch -> ( th -> ( ps -> ta ) ) )   =>    |- ( ch -> ( th -> ( ph -> ta ) ) )
Theorem	syl6d 70	A nested syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by O'Cat, 2-Feb-2006.) (Revised by NM, 3-Feb-2006.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( ph -> ( th -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ta ) ) )
Theorem	syl8 71	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( th -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ta ) ) )
Theorem	syl9 72	A nested syllogism inference with different antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ch -> ta ) )   =>    |- ( ph -> ( th -> ( ps -> ta ) ) )
Theorem	syl9r 73	A nested syllogism inference with different antecedents. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ch -> ta ) )   =>    |- ( th -> ( ph -> ( ps -> ta ) ) )
Theorem	imim12d 74	Deduction combining antecedents and consequents. (Contributed by NM, 7-Aug-1994.) (Proof shortened by O'Cat, 30-Oct-2011.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ta ) )   =>    |- ( ph -> ( ( ch -> th ) -> ( ps -> ta ) ) )
Theorem	imim1d 75	Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )
Theorem	imim1 76	A closed form of syllogism (see syl 14). Theorem *2.06 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)
|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
Theorem	pm2.83 77	Theorem *2.83 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ( ch -> th ) ) -> ( ph -> ( ps -> th ) ) ) )
Theorem	com23 78	Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ch -> ( ps -> th ) ) )
Theorem	com3r 79	Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ch -> ( ph -> ( ps -> th ) ) )
Theorem	com13 80	Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ch -> ( ps -> ( ph -> th ) ) )
Theorem	com3l 81	Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ps -> ( ch -> ( ph -> th ) ) )
Theorem	pm2.04 82	Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) )
Theorem	com34 83	Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ps -> ( th -> ( ch -> ta ) ) ) )
Theorem	com4l 84	Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by O'Cat, 15-Aug-2004.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ps -> ( ch -> ( th -> ( ph -> ta ) ) ) )
Theorem	com4t 85	Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ch -> ( th -> ( ph -> ( ps -> ta ) ) ) )
Theorem	com4r 86	Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( th -> ( ph -> ( ps -> ( ch -> ta ) ) ) )
Theorem	com24 87	Commutation of antecedents. Swap 2nd and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( th -> ( ch -> ( ps -> ta ) ) ) )
Theorem	com14 88	Commutation of antecedents. Swap 1st and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( th -> ( ps -> ( ch -> ( ph -> ta ) ) ) )
Theorem	com45 89	Commutation of antecedents. Swap 4th and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ( ta -> ( th -> et ) ) ) ) )
Theorem	com35 90	Commutation of antecedents. Swap 3rd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ph -> ( ps -> ( ta -> ( th -> ( ch -> et ) ) ) ) )
Theorem	com25 91	Commutation of antecedents. Swap 2nd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ph -> ( ta -> ( ch -> ( th -> ( ps -> et ) ) ) ) )
Theorem	com5l 92	Commutation of antecedents. Rotate left. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ps -> ( ch -> ( th -> ( ta -> ( ph -> et ) ) ) ) )
Theorem	com15 93	Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ta -> ( ps -> ( ch -> ( th -> ( ph -> et ) ) ) ) )
Theorem	com52l 94	Commutation of antecedents. Rotate left twice. (Contributed by Jeff Hankins, 28-Jun-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ch -> ( th -> ( ta -> ( ph -> ( ps -> et ) ) ) ) )
Theorem	com52r 95	Commutation of antecedents. Rotate right twice. (Contributed by Jeff Hankins, 28-Jun-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( th -> ( ta -> ( ph -> ( ps -> ( ch -> et ) ) ) ) )
Theorem	com5r 96	Commutation of antecedents. Rotate right. (Contributed by Wolf Lammen, 29-Jul-2012.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ta -> ( ph -> ( ps -> ( ch -> ( th -> et ) ) ) ) )
Theorem	jarr 97	Elimination of a nested antecedent. (Contributed by Wolf Lammen, 9-May-2013.)
|- ( ( ( ph -> ps ) -> ch ) -> ( ps -> ch ) )
Theorem	pm2.86i 98	Inference based on pm2.86 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
|- ( ( ph -> ps ) -> ( ph -> ch ) )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	pm2.86d 99	Deduction based on pm2.86 100. (Contributed by NM, 29-Jun-1995.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
|- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	pm2.86 100	Converse of Axiom ax-2 7. Theorem *2.86 of [WhiteheadRussell] p. 108. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
|- ( ( ( ph -> ps ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) )