P. 13 of Theorem List - Intuitionistic Logic Explorer

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1201-1300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3impdi 1201	Importation inference (undistribute conjunction).
|- (((ph /\ ps) /\ (ph /\ ch)) -> th)   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	3impdir 1202	Importation inference (undistribute conjunction).
|- (((ph /\ ps) /\ (ch /\ ps)) -> th)   =>   |- ((ph /\ ch /\ ps) -> th)
Theorem	3anidm12 1203	Inference from idempotent law for conjunction.
|- ((ph /\ ph /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	3anidm13 1204	Inference from idempotent law for conjunction.
|- ((ph /\ ps /\ ph) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	3anidm23 1205	Inference from idempotent law for conjunction.
|- ((ph /\ ps /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	3ori 1206	Infer implication from triple disjunction.
|- (ph \/ ps \/ ch)   =>   |- ((-. ph /\ -. ps) -> ch)
Theorem	3jao 1207	Disjunction of 3 antecedents.
|- (((ph -> ps) /\ (ch -> ps) /\ (th -> ps)) -> ((ph \/ ch \/ th) -> ps))
Theorem	3jaob 1208	Disjunction of 3 antecedents.
|- (((ph \/ ch \/ th) -> ps) <-> ((ph -> ps) /\ (ch -> ps) /\ (th -> ps)))
Theorem	3jaoi 1209	Disjunction of 3 antecedents (inference).
|- (ph -> ps)   &   |- (ch -> ps)   &   |- (th -> ps)   =>   |- ((ph \/ ch \/ th) -> ps)
Theorem	3jaod 1210	Disjunction of 3 antecedents (deduction).
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ch))   &   |- (ph -> (ta -> ch))   =>   |- (ph -> ((ps \/ th \/ ta) -> ch))
Theorem	3jaoian 1211	Disjunction of 3 antecedents (inference).
|- ((ph /\ ps) -> ch)   &   |- ((th /\ ps) -> ch)   &   |- ((ta /\ ps) -> ch)   =>   |- (((ph \/ th \/ ta) /\ ps) -> ch)
Theorem	3jaodan 1212	Disjunction of 3 antecedents (deduction).
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ th) -> ch)   &   |- ((ph /\ ta) -> ch)   =>   |- ((ph /\ (ps \/ th \/ ta)) -> ch)
Theorem	3jaao 1213	Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (The proof was shortened by Andrew Salmon, 13-May-2011.)
|- (ph -> (ps -> ch))   &   |- (th -> (ta -> ch))   &   |- (et -> (ze -> ch))   =>   |- ((ph /\ th /\ et) -> ((ps \/ ta \/ ze) -> ch))
Theorem	syl3an9b 1214	Nested syllogism inference conjoining 3 dissimilar antecedents.
|- (ph -> (ps <-> ch))   &   |- (th -> (ch <-> ta))   &   |- (et -> (ta <-> ze))   =>   |- ((ph /\ th /\ et) -> (ps <-> ze))
Theorem	3orbi123d 1215	Deduction joining 3 equivalences to form equivalence of disjunctions.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   &   |- (ph -> (et <-> ze))   =>   |- (ph -> ((ps \/ th \/ et) <-> (ch \/ ta \/ ze)))
Theorem	3anbi123d 1216	Deduction joining 3 equivalences to form equivalence of conjunctions.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   &   |- (ph -> (et <-> ze))   =>   |- (ph -> ((ps /\ th /\ et) <-> (ch /\ ta /\ ze)))
Theorem	3anbi12d 1217	Deduction conjoining and adding a conjunct to equivalences.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> ((ps /\ th /\ et) <-> (ch /\ ta /\ et)))
Theorem	3anbi13d 1218	Deduction conjoining and adding a conjunct to equivalences.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> ((ps /\ et /\ th) <-> (ch /\ et /\ ta)))
Theorem	3anbi23d 1219	Deduction conjoining and adding a conjunct to equivalences.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> ((et /\ ps /\ th) <-> (et /\ ch /\ ta)))
Theorem	3anbi1d 1220	Deduction adding conjuncts to an equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((ps /\ th /\ ta) <-> (ch /\ th /\ ta)))
Theorem	3anbi2d 1221	Deduction adding conjuncts to an equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th /\ ps /\ ta) <-> (th /\ ch /\ ta)))
Theorem	3anbi3d 1222	Deduction adding conjuncts to an equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th /\ ta /\ ps) <-> (th /\ ta /\ ch)))
Theorem	3anim123d 1223	Deduction joining 3 implications to form implication of conjunctions.
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   &   |- (ph -> (et -> ze))   =>   |- (ph -> ((ps /\ th /\ et) -> (ch /\ ta /\ ze)))
Theorem	3orim123d 1224	Deduction joining 3 implications to form implication of disjunctions.
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   &   |- (ph -> (et -> ze))   =>   |- (ph -> ((ps \/ th \/ et) -> (ch \/ ta \/ ze)))
Theorem	an6 1225	Rearrangement of 6 conjuncts.
|- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> ((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)))
Theorem	3an6 1226	Analog of an4 502 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (((ph /\ ps) /\ (ch /\ th) /\ (ta /\ et)) <-> ((ph /\ ch /\ ta) /\ (ps /\ th /\ et)))
Theorem	3or6 1227	Analog of or4 664 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
|- (((ph \/ ps) \/ (ch \/ th) \/ (ta \/ et)) <-> ((ph \/ ch \/ ta) \/ (ps \/ th \/ et)))
Theorem	mp3an1 1228	An inference based on modus ponens.
|- ph   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ps /\ ch) -> th)
Theorem	mp3an2 1229	An inference based on modus ponens.
|- ps   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mp3an3 1230	An inference based on modus ponens.
|- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mp3an12 1231	An inference based on modus ponens.
|- ph   &   |- ps   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ch -> th)
Theorem	mp3an13 1232	An inference based on modus ponens.
|- ph   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ps -> th)
Theorem	mp3an23 1233	An inference based on modus ponens.
|- ps   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	mp3an1i 1234	An inference based on modus ponens.
|- ps   &   |- (ph -> ((ps /\ ch /\ th) -> ta))   =>   |- (ph -> ((ch /\ th) -> ta))
Theorem	mp3anl1 1235	An inference based on modus ponens.
|- ph   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ps /\ ch) /\ th) -> ta)
Theorem	mp3anl2 1236	An inference based on modus ponens.
|- ps   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ph /\ ch) /\ th) -> ta)
Theorem	mp3anl3 1237	An inference based on modus ponens.
|- ch   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ph /\ ps) /\ th) -> ta)
Theorem	mp3anr1 1238	An inference based on modus ponens.
|- ps   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ch /\ th)) -> ta)
Theorem	mp3anr2 1239	An inference based on modus ponens.
|- ch   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ th)) -> ta)
Theorem	mp3anr3 1240	An inference based on modus ponens.
|- th   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ ch)) -> ta)
Theorem	mp3an 1241	An inference based on modus ponens.
|- ph   &   |- ps   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- th
Theorem	mpd3an3 1242	An inference based on modus ponens.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mpd3an23 1243	An inference based on modus ponens.
|- (ph -> ps)   &   |- (ph -> ch)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	biimp3a 1244	Infer implication from a logical equivalence. Similar to biimpa 279.
|- ((ph /\ ps) -> (ch <-> th))   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	biimp3ar 1245	Infer implication from a logical equivalence. Similar to biimpar 280.
|- ((ph /\ ps) -> (ch <-> th))   =>   |- ((ph /\ ps /\ th) -> ch)
Theorem	3anandis 1246	Inference that undistributes a triple conjunction in the antecedent.
|- (((ph /\ ps) /\ (ph /\ ch) /\ (ph /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ ch /\ th)) -> ta)
Theorem	3anandirs 1247	Inference that undistributes a triple conjunction in the antecedent.
|- (((ph /\ th) /\ (ps /\ th) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ps /\ ch) /\ th) -> ta)
Theorem	ecase23d 1248	Deduction for elimination by cases.
|- (ph -> -. ch)   &   |- (ph -> -. th)   &   |- (ph -> (ps \/ ch \/ th))   =>   |- (ph -> ps)
Theorem	3ecase 1249	Inference for elimination by cases.
|- (-. ph -> th)   &   |- (-. ps -> th)   &   |- (-. ch -> th)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- th
1.3  Other axiomatizations of classical propositional calculus
1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom
Theorem	meredith 1250	Carew Meredith's sole axiom for propositional calculus. This amazing formula is thought to be the shortest possible single axiom for propositional calculus with inference rule ax-mp 8, where negation and implication are primitive. Here we prove Meredith's axiom from ax-1 5, ax-2 6, and ax-3 7. Then from it we derive the Lukasiewicz axioms luk-1 1265, luk-2 1266, and luk-3 1267. Using these we finally re-derive our axioms as ax1 1276, ax2 1277, and ax3 1278, thus proving the equivalence of all three systems. C. A. Meredith, "Single Axioms for the Systems (C,N), (C,O) and (A,N) of the Two-Valued Propositional Calculus," The Journal of Computing Systems vol. 1 (1953), pp. 155-164. Meredith claimed to be close to a proof that this axiom is the shortest possible, but the proof was apparently never completed. An obscure Irish lecturer, Meredith (1904-1976) became enamored with logic somewhat late in life after attending talks by Lukasiewicz and produced many remarkable results such as this axiom. From his obituary: "He did logic whenever time and opportunity presented themselves, and he did it on whatever materials came to hand: in a pub, his favored pint of porter within reach, he would use the inside of cigarette packs to write proofs for logical colleagues." (The proof was shortened by Andrew Salmon, 25-Jul-2011.) (The proof was shortened by Wolf Lammen, 28-May-2013.)
|- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta) -> ((ta -> ph) -> (th -> ph)))
Axiom	ax-meredith 1251	Theorem meredith 1250 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1276, ax2 1277, and ax3 1278 below depend only on Meredith's sole axiom and not accidentally on a previous theorem above. Outside of this section, we will not make use of this axiom.
|- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta) -> ((ta -> ph) -> (th -> ph)))
Theorem	merlem1 1252	Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.)
|- (((ch -> (-. ph -> ps)) -> ta) -> (ph -> ta))
Theorem	merlem2 1253	Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ph -> ph) -> ch) -> (th -> ch))
Theorem	merlem3 1254	Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ps -> ch) -> ph) -> (ch -> ph))
Theorem	merlem4 1255	Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ta -> ((ta -> ph) -> (th -> ph)))
Theorem	merlem5 1256	Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> ps) -> (-. -. ph -> ps))
Theorem	merlem6 1257	Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ch -> (((ps -> ch) -> ph) -> (th -> ph)))
Theorem	merlem7 1258	Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ph -> (((ps -> ch) -> th) -> (((ch -> ta) -> (-. th -> -. ps)) -> th)))
Theorem	merlem8 1259	Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ps -> ch) -> th) -> (((ch -> ta) -> (-. th -> -. ps)) -> th))
Theorem	merlem9 1260	Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ph -> ps) -> (ch -> (th -> (ps -> ta)))) -> (et -> (ch -> (th -> (ps -> ta)))))
Theorem	merlem10 1261	Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> (ph -> ps)) -> (th -> (ph -> ps)))
Theorem	merlem11 1262	Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> (ph -> ps)) -> (ph -> ps))
Theorem	merlem12 1263	Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((th -> (-. -. ch -> ch)) -> ph) -> ph)
Theorem	merlem13 1264	Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> ps) -> (((th -> (-. -. ch -> ch)) -> -. -. ph) -> ps))
Theorem	luk-1 1265	1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
|- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))
Theorem	luk-2 1266	2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
|- ((-. ph -> ph) -> ph)
Theorem	luk-3 1267	3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
|- (ph -> (-. ph -> ps))
1.3.2  Derive the standard axioms from the Lukasiewicz axioms
Theorem	luklem1 1268	Used to rederive standard propositional axioms from Lukasiewicz'.
|- (ph -> ps)   &   |- (ps -> ch)   =>   |- (ph -> ch)
Theorem	luklem2 1269	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> -. ps) -> (((ph -> ch) -> th) -> (ps -> th)))
Theorem	luklem3 1270	Used to rederive standard propositional axioms from Lukasiewicz'.
|- (ph -> (((-. ph -> ps) -> ch) -> (th -> ch)))
Theorem	luklem4 1271	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((((-. ph -> ph) -> ph) -> ps) -> ps)
Theorem	luklem5 1272	Used to rederive standard propositional axioms from Lukasiewicz'.
|- (ph -> (ps -> ph))
Theorem	luklem6 1273	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> (ph -> ps)) -> (ph -> ps))
Theorem	luklem7 1274	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> (ps -> ch)) -> (ps -> (ph -> ch)))
Theorem	luklem8 1275	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> ps) -> ((ch -> ph) -> (ch -> ps)))
Theorem	ax1 1276	Standard propositional axiom derived from Lukasiewicz axioms.
|- (ph -> (ps -> ph))
Theorem	ax2 1277	Standard propositional axiom derived from Lukasiewicz axioms.
|- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
Theorem	ax3 1278	Standard propositional axiom derived from Lukasiewicz axioms.
|- ((-. ph -> -. ps) -> (ps -> ph))
1.3.3  Logical 'nand' (Sheffer stroke)
Syntax	wnand 1279	Extend wff definition to include 'nand'.
wff (ph -/\ ps)
Definition	df-nand 1280	Define incompatibility ('not-and' or 'nand'). This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar.
|- ((ph -/\ ps) <-> -. (ph /\ ps))
1.3.4  Derive Nicod's axiom from the standard axioms
Theorem	nic-justlem 1281	Lemma for handling nested 'nand's.
|- ((ph -/\ (ch -/\ ps)) <-> (ph -> (ch /\ ps)))
Theorem	nic-justim 1282	Show equivalence between implication and the Nicod version. To derive nic-dfim 1285, apply nic-justbi 1284.
|- ((ph -> ps) <-> (ph -/\ (ps -/\ ps)))
Theorem	nic-justneg 1283	Show equivalence between negation and the Nicod version. To derive nic-dfneg 1286, apply nic-justbi 1284.
|- (-. ps <-> (ps -/\ ps))
Theorem	nic-justbi 1284	Show equivalence between the bidirectional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph <-> ps) <-> ((ph -/\ ps) -/\ ((ph -/\ ph) -/\ (ps -/\ ps))))
Theorem	nic-dfim 1285	Define implication in terms of 'nand'. Analogous to ((ph -/\ (ps -/\ ps)) <-> (ph -> ps)). In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement).
|- (((ph -/\ (ps -/\ ps)) -/\ (ph -> ps)) -/\ (((ph -/\ (ps -/\ ps)) -/\ (ph -/\ (ps -/\ ps))) -/\ ((ph -> ps) -/\ (ph -> ps))))
Theorem	nic-dfneg 1286	Define negation in terms of 'nand'. Analogous to ((ph -/\ ph) <-> -. ph). In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement).
|- (((ph -/\ ph) -/\ -. ph) -/\ (((ph -/\ ph) -/\ (ph -/\ ph)) -/\ (-. ph -/\ -. ph)))
Theorem	nic-mp 1287	Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply ch, this form is necessary for useful derivations from nic-ax 1289. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ph   &   |- (ph -/\ (ch -/\ ps))   =>   |- ps
Theorem	nic-mpALT 1288	A direct proof of nic-mp 1287.
|- ph   &   |- (ph -/\ (ch -/\ ps))   =>   |- ps
Theorem	nic-ax 1289	Nicod's axiom derived from the standard ones. See _Intro. to Math. Phil._ by B. Russell, p. 152. Like meredith 1250, the usual axioms can be derived from this and vice versa. Unlike meredith 1250, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1289, nic-mp 1287 } is equivalent to { luk-1 1265, luk-2 1266, luk-3 1267, ax-mp 8 }. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
Theorem	nic-axALT 1290	A direct proof of nic-ax 1289.
|- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
1.3.5  Derive the Lukasiewicz axioms from Nicod's axiom
Theorem	nic-imp 1291	Inference for nic-mp 1287 using nic-ax 1289 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ch -/\ ps))   =>   |- ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))
Theorem	nic-idlem1 1292	Lemma for nic-id 1294.
|- ((th -/\ (ta -/\ (ta -/\ ta))) -/\ (((ph -/\ (ch -/\ ps)) -/\ th) -/\ ((ph -/\ (ch -/\ ps)) -/\ th)))
Theorem	nic-idlem2 1293	Lemma for nic-id 1294. Inference used by nic-id 1294.
|- (et -/\ ((ph -/\ (ch -/\ ps)) -/\ th))   =>   |- ((th -/\ (ta -/\ (ta -/\ ta))) -/\ et)
Theorem	nic-id 1294	Theorem id 18 expressed with -/\. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ta -/\ (ta -/\ ta))
Theorem	nic-swap 1295	-/\ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- ((th -/\ ph) -/\ ((ph -/\ th) -/\ (ph -/\ th)))
Theorem	nic-isw1 1296	Inference version of nic-swap 1295. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (th -/\ ph)   =>   |- (ph -/\ th)
Theorem	nic-isw2 1297	Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ps -/\ (th -/\ ph))   =>   |- (ps -/\ (ph -/\ th))
Theorem	nic-iimp1 1298	Inference version of nic-imp 1291 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ch -/\ ps))   &   |- (th -/\ ch)   =>   |- (th -/\ ph)
Theorem	nic-iimp2 1299	Inference version of nic-imp 1291 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- ((ph -/\ ps) -/\ (ch -/\ ch))   &   |- (th -/\ ph)   =>   |- (th -/\ (ch -/\ ch))
Theorem	nic-idel 1300	Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ch -/\ ps))   =>   |- (ph -/\ (ch -/\ ch))