P. 14 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 1301-1400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xor2 1301	Two ways to express "exclusive or." (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
Theorem	xorneg1 1302	\/_ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( -. ph \/_ ps ) <-> -. ( ph \/_ ps ) )
Theorem	xorneg2 1303	\/_ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph \/_ -. ps ) <-> -. ( ph \/_ ps ) )
Theorem	xorneg 1304	\/_ is unchanged under negation of both arguments. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( -. ph \/_ -. ps ) <-> ( ph \/_ ps ) )
Theorem	xorbi12i 1305	Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph \/_ ch ) <-> ( ps \/_ th ) )
Theorem	xorbi12d 1306	Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps \/_ th ) <-> ( ch \/_ ta ) ) )
1.2.11  True and false constants
Syntax	wtru 1307	T. is a wff.
wff T.
Syntax	wfal 1308	F. is a wff.
wff F.
Theorem	trujust 1309	Soundness justification theorem for df-tru 1310. (Contributed by Mario Carneiro, 17-Nov-2013.)
|- ( ( ph <-> ph ) <-> ( ps <-> ps ) )
Definition	df-tru 1310	Definition of T., a tautology. T. is a constant true. In this definition biid 227 is used as an antecedent, however, any true wff, such as an axiom, can be used in its place. (Contributed by Anthony Hart, 13-Oct-2010.)
|- ( T. <-> ( ph <-> ph ) )
Definition	df-fal 1311	Definition of F., a contradiction. F. is a constant false. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( F. <-> -. T. )
Theorem	tru 1312	T. is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
|- T.
Theorem	fal 1313	F. is not provable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
|- -. F.
Theorem	trud 1314	Eliminate T. as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( T. -> ph )   =>    |- ph
Theorem	tbtru 1315	If something is true, it outputs T.. (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( ph <-> ( ph <-> T. ) )
Theorem	nbfal 1316	If something is not true, it outputs F.. (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( -. ph <-> ( ph <-> F. ) )
Theorem	bitru 1317	A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.)
|- ph   =>    |- ( ph <-> T. )
Theorem	bifal 1318	A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.)
|- -. ph   =>    |- ( ph <-> F. )
Theorem	falim 1319	F. implies anything. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
|- ( F. -> ph )
Theorem	falimd 1320	F. implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ F. ) -> ps )
Theorem	a1tru 1321	Anything implies T.. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
|- ( ph -> T. )
Theorem	dfnot 1322	Given falsum, we can define the negation of a wff ph as the statement that a contradiction follows from assuming ph. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( -. ph <-> ( ph -> F. ) )
Theorem	inegd 1323	Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ ps ) -> F. )   =>    |- ( ph -> -. ps )
Theorem	efald 1324	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ -. ps ) -> F. )   =>    |- ( ph -> ps )
Theorem	pm2.21fal 1325	If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> ps )   &    |- ( ph -> -. ps )   =>    |- ( ph -> F. )
1.2.12  Truth tables Some sources define operations on true/false values using truth tables. These tables show the results of their operations for all possible combinations of true ( T.) and false ( F.). Here we show that our definitions and axioms produce equivalent results for /\ (conjunction aka logical 'and') df-an 360, \/ (disjunction aka logical inclusive 'or') df-or 359, -> (implies) wi 4, -. (not) wn 3, <-> (logical equivalence) df-bi 177, -/\ (nand aka Sheffer stroke) df-nan 1288, and \/_ (exclusive or) df-xor 1296.
Theorem	truantru 1326	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. /\ T. ) <-> T. )
Theorem	truanfal 1327	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. /\ F. ) <-> F. )
Theorem	falantru 1328	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. /\ T. ) <-> F. )
Theorem	falanfal 1329	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. /\ F. ) <-> F. )
Theorem	truortru 1330	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. \/ T. ) <-> T. )
Theorem	truorfal 1331	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. \/ F. ) <-> T. )
Theorem	falortru 1332	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. \/ T. ) <-> T. )
Theorem	falorfal 1333	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. \/ F. ) <-> F. )
Theorem	truimtru 1334	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. -> T. ) <-> T. )
Theorem	truimfal 1335	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -> F. ) <-> F. )
Theorem	falimtru 1336	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. -> T. ) <-> T. )
Theorem	falimfal 1337	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. -> F. ) <-> T. )
Theorem	nottru 1338	A -. identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( -. T. <-> F. )
Theorem	notfal 1339	A -. identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( -. F. <-> T. )
Theorem	trubitru 1340	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. <-> T. ) <-> T. )
Theorem	trubifal 1341	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. <-> F. ) <-> F. )
Theorem	falbitru 1342	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. <-> T. ) <-> F. )
Theorem	falbifal 1343	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. <-> F. ) <-> T. )
Theorem	trunantru 1344	A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -/\ T. ) <-> F. )
Theorem	trunanfal 1345	A -/\ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -/\ F. ) <-> T. )
Theorem	falnantru 1346	A -/\ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. -/\ T. ) <-> T. )
Theorem	falnanfal 1347	A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. -/\ F. ) <-> T. )
Theorem	truxortru 1348	A \/_ identity. (Contributed by David A. Wheeler, 8-May-2015.)
|- ( ( T. \/_ T. ) <-> F. )
Theorem	truxorfal 1349	A \/_ identity. (Contributed by David A. Wheeler, 8-May-2015.)
|- ( ( T. \/_ F. ) <-> T. )
Theorem	falxortru 1350	A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015.)
|- ( ( F. \/_ T. ) <-> T. )
Theorem	falxorfal 1351	A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015.)
|- ( ( F. \/_ F. ) <-> F. )
1.2.13  Auxiliary theorems for Alan Sare's virtual deduction tool, part 1
Theorem	ee22 1352	Virtual deduction rule e22 28443 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 2-May-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ch -> ( th -> ta ) )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	ee12an 1353	e12an 28500 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) TODO: this is frequently used; come up with better label.
|- ( ph -> ps )   &    |- ( ph -> ( ch -> th ) )   &    |- ( ( ps /\ th ) -> ta )   =>    |- ( ph -> ( ch -> ta ) )
Theorem	ee23 1354	e23 28530 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> ( th -> ta ) ) )   &    |- ( ch -> ( ta -> et ) )   =>    |- ( ph -> ( ps -> ( th -> et ) ) )
Theorem	exbir 1355	Exportation implication also converting head from biconditional to conditional. This proof is exbirVD 28629 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )
Theorem	3impexp 1356	impexp 433 with a 3-conjunct antecedent. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( ( ( ph /\ ps /\ ch ) -> th ) <-> ( ph -> ( ps -> ( ch -> th ) ) ) )
Theorem	3impexpbicom 1357	3impexp 1356 with biconditional consequent of antecedent that is commuted in consequent. Derived automatically from 3impexpVD 28632. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) <-> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )
Theorem	3impexpbicomi 1358	Deduction form of 3impexpbicom 1357. Derived automatically from 3impexpbicomiVD 28634. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) )
Theorem	ancomsimp 1359	Closed form of ancoms 439. Derived automatically from ancomsimpVD 28641. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( ( ( ph /\ ps ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )
Theorem	exp3acom3r 1360	Export and commute antecedents. (Contributed by Alan Sare, 18-Mar-2012.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ps -> ( ch -> ( ph -> th ) ) )
Theorem	exp3acom23g 1361	Implication form of exp3acom23 1362. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ( ph -> ( ( ps /\ ch ) -> th ) ) <-> ( ph -> ( ch -> ( ps -> th ) ) ) )
Theorem	exp3acom23 1362	The exportation deduction exp3a 425 with commutation of the conjoined wwfs. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> ( ch -> ( ps -> th ) ) )
Theorem	simplbi2comg 1363	Implication form of simplbi2com 1364. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ( ph <-> ( ps /\ ch ) ) -> ( ch -> ( ps -> ph ) ) )
Theorem	simplbi2com 1364	A deduction eliminating a conjunct, similar to simplbi2 608. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ps -> ph ) )
Theorem	ee21 1365	e21 28505 without virtual deductions. (Contributed by Alan Sare, 18-Mar-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> th )   &    |- ( ch -> ( th -> ta ) )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	ee10 1366	e10 28467 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) TODO: this is frequently used; come up with better label.
|- ( ph -> ps )   &    |- ch   &    |- ( ps -> ( ch -> th ) )   =>    |- ( ph -> th )
Theorem	ee02 1367	e02 28470 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping.
|- ph   &    |- ( ps -> ( ch -> th ) )   &    |- ( ph -> ( th -> ta ) )   =>    |- ( ps -> ( ch -> ta ) )
1.2.14  Half-adders and full adders in propositional calculus Propositional calculus deals with truth values, which can be interpreted as bits. Using this, we can define the half-adder in pure propositional calculus, and show its basic properties.
Syntax	whad 1368	Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.)
wff hadd ( ph , ps , ch )
Syntax	wcad 1369	Define the half adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
wff cadd ( ph , ps , ch )
Definition	df-had 1370	Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )
Definition	df-cad 1371	Define the half adder carry, which is true when at least two arguments are true. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )
Theorem	hadbi123d 1372	Equality theorem for half adder. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   &    |- ( ph -> ( et <-> ze ) )   =>    |- ( ph -> (hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) ) )
Theorem	cadbi123d 1373	Equality theorem for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   &    |- ( ph -> ( et <-> ze ) )   =>    |- ( ph -> (cadd ( ps , th , et ) <-> cadd ( ch , ta , ze ) ) )
Theorem	hadbi123i 1374	Equality theorem for half adder. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- (hadd ( ph , ch , ta ) <-> hadd ( ps , th , et ) )
Theorem	cadbi123i 1375	Equality theorem for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- (cadd ( ph , ch , ta ) <-> cadd ( ps , th , et ) )
Theorem	hadass 1376	Associative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )
Theorem	hadbi 1377	The half adder is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> ch ) )
Theorem	hadcoma 1378	Commutative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ps , ph , ch ) )
Theorem	hadcomb 1379	Commutative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ph , ch , ps ) )
Theorem	hadrot 1380	Rotation law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ps , ch , ph ) )
Theorem	cador 1381	Write the adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) )
Theorem	cadan 1382	Write the adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) )
Theorem	hadnot 1383	The half adder distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( -. hadd ( ph , ps , ch ) <-> hadd ( -. ph , -. ps , -. ch ) )
Theorem	cadnot 1384	The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( -. cadd ( ph , ps , ch ) <-> cadd ( -. ph , -. ps , -. ch ) )
Theorem	cadcoma 1385	Commutative law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> cadd ( ps , ph , ch ) )
Theorem	cadcomb 1386	Commutative law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> cadd ( ph , ch , ps ) )
Theorem	cadrot 1387	Rotation law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> cadd ( ps , ch , ph ) )
Theorem	cad1 1388	If one parameter is true, the adder carry is true exactly when at least one of the other parameters is true. (Contributed by Mario Carneiro, 8-Sep-2016.)
|- ( ch -> (cadd ( ph , ps , ch ) <-> ( ph \/ ps ) ) )
Theorem	cad11 1389	If two parameters are true, the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph /\ ps ) -> cadd ( ph , ps , ch ) )
Theorem	cad0 1390	If one parameter is false, the adder carry is true exactly when both of the other two parameters are true. (Contributed by Mario Carneiro, 8-Sep-2016.)
|- ( -. ch -> (cadd ( ph , ps , ch ) <-> ( ph /\ ps ) ) )
Theorem	cadtru 1391	Rotation law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- cadd ( T. , T. , ph )
Theorem	had1 1392	If the first parameter is true, the half adder is equivalent to the equality of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph -> (hadd ( ph , ps , ch ) <-> ( ps <-> ch ) ) )
Theorem	had0 1393	If the first parameter is false, the half adder is equivalent to the XOR of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( -. ph -> (hadd ( ph , ps , ch ) <-> ( ps \/_ ch ) ) )
1.3  Other axiomatizations of classical propositional calculus
1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom
Theorem	meredith 1394	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 1410, luk-2 1411, and luk-3 1412. Using these we finally re-derive our axioms as ax1 1421, ax2 1422, and ax3 1423, 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." (Contributed by NM, 14-Dec-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Wolf Lammen, 28-May-2013.)
|- ( ( ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ta ) -> ( ( ta -> ph ) -> ( th -> ph ) ) )
Theorem	axmeredith 1395	Alias for meredith 1394 which "verify markup *" will match to ax-meredith 1396. (Contributed by NM, 21-Aug-2017.) (New usage is discouraged.)
|- ( ( ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ta ) -> ( ( ta -> ph ) -> ( th -> ph ) ) )
Axiom	ax-meredith 1396	Theorem meredith 1394 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1421, ax2 1422, and ax3 1423 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. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ta ) -> ( ( ta -> ph ) -> ( th -> ph ) ) )
Theorem	merlem1 1397	Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.) (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ch -> ( -. ph -> ps ) ) -> ta ) -> ( ph -> ta ) )
Theorem	merlem2 1398	Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ph -> ph ) -> ch ) -> ( th -> ch ) )
Theorem	merlem3 1399	Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ps -> ch ) -> ph ) -> ( ch -> ph ) )
Theorem	merlem4 1400	Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ta -> ( ( ta -> ph ) -> ( th -> ph ) ) )