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	nanim 1301	Show equivalence between implication and the Nicod version. To derive nic-dfim 1443, apply nanbi 1303. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ( ( ph -> ps ) <-> ( ph -/\ ( ps -/\ ps ) ) )
Theorem	nannot 1302	Show equivalence between negation and the Nicod version. To derive nic-dfneg 1444, apply nanbi 1303. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ( -. ps <-> ( ps -/\ ps ) )
Theorem	nanbi 1303	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	nanbi1 1304	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ( ( ph <-> ps ) -> ( ( ph -/\ ch ) <-> ( ps -/\ ch ) ) )
Theorem	nanbi2 1305	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ( ( ph <-> ps ) -> ( ( ch -/\ ph ) <-> ( ch -/\ ps ) ) )
Theorem	nanbi12 1306	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ph -/\ ch ) <-> ( ps -/\ th ) ) )
Theorem	nanbi1i 1307	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ( ph <-> ps )   =>    |- ( ( ph -/\ ch ) <-> ( ps -/\ ch ) )
Theorem	nanbi2i 1308	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ( ph <-> ps )   =>    |- ( ( ch -/\ ph ) <-> ( ch -/\ ps ) )
Theorem	nanbi12i 1309	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph -/\ ch ) <-> ( ps -/\ th ) )
Theorem	nanbi1d 1310	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps -/\ th ) <-> ( ch -/\ th ) ) )
Theorem	nanbi2d 1311	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th -/\ ps ) <-> ( th -/\ ch ) ) )
Theorem	nanbi12d 1312	Join two logical equivalences with anti-conjunction. (Contributed by Scott Fenton, 2-Jan-2018.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps -/\ th ) <-> ( ch -/\ ta ) ) )
1.2.10  Logical 'xor'
Syntax	wxo 1313	Extend wff definition to include exclusive disjunction ('xor').
wff ( ph \/_ ps )
Definition	df-xor 1314	Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. After we define the constant true T. (df-tru 1328) and the constant false F. (df-fal 1329), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1367), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1368), ( ( F. \/_ T. ) <-> T. ) (falxortru 1369), and ( ( F. \/_ F. ) <-> F. ) (falxorfal 1370). Contrast with /\ (df-an 361), \/ (df-or 360), -> (wi 4), and -/\ (df-nan 1297) . (Contributed by FL, 22-Nov-2010.)
|- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
Theorem	xnor 1315	Two ways to write XNOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph <-> ps ) <-> -. ( ph \/_ ps ) )
Theorem	xorcom 1316	\/_ is commutative. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph \/_ ps ) <-> ( ps \/_ ph ) )
Theorem	xorass 1317	\/_ is associative. (Contributed by FL, 22-Nov-2010.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- ( ( ( ph \/_ ps ) \/_ ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )
Theorem	excxor 1318	This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010.)
|- ( ( ph \/_ ps ) <-> ( ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) )
Theorem	xor2 1319	Two ways to express "exclusive or." (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
Theorem	xorneg1 1320	\/_ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( -. ph \/_ ps ) <-> -. ( ph \/_ ps ) )
Theorem	xorneg2 1321	\/_ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph \/_ -. ps ) <-> -. ( ph \/_ ps ) )
Theorem	xorneg 1322	\/_ is unchanged under negation of both arguments. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( -. ph \/_ -. ps ) <-> ( ph \/_ ps ) )
Theorem	xorbi12i 1323	Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph \/_ ch ) <-> ( ps \/_ th ) )
Theorem	xorbi12d 1324	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 1325	T. is a wff.
wff T.
Syntax	wfal 1326	F. is a wff.
wff F.
Theorem	trujust 1327	Soundness justification theorem for df-tru 1328. (Contributed by Mario Carneiro, 17-Nov-2013.)
|- ( ( ph <-> ph ) <-> ( ps <-> ps ) )
Definition	df-tru 1328	Definition of T., a tautology. T. is a constant true. In this definition biid 228 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 1329	Definition of F., a contradiction. F. is a constant false. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( F. <-> -. T. )
Theorem	tru 1330	T. is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
|- T.
Theorem	fal 1331	F. is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
|- -. F.
Theorem	trud 1332	Eliminate T. as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( T. -> ph )   =>    |- ph
Theorem	tbtru 1333	If something is true, it outputs T.. (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( ph <-> ( ph <-> T. ) )
Theorem	nbfal 1334	If something is not true, it outputs F.. (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( -. ph <-> ( ph <-> F. ) )
Theorem	bitru 1335	A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.)
|- ph   =>    |- ( ph <-> T. )
Theorem	bifal 1336	A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.)
|- -. ph   =>    |- ( ph <-> F. )
Theorem	falim 1337	F. implies anything. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
|- ( F. -> ph )
Theorem	falimd 1338	F. implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ F. ) -> ps )
Theorem	a1tru 1339	Anything implies T.. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
|- ( ph -> T. )
Theorem	truan 1340	True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.)
|- ( ( T. /\ ph ) <-> ph )
Theorem	dfnot 1341	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 1342	Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ ps ) -> F. )   =>    |- ( ph -> -. ps )
Theorem	efald 1343	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ -. ps ) -> F. )   =>    |- ( ph -> ps )
Theorem	pm2.21fal 1344	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 361, \/ (disjunction aka logical inclusive 'or') df-or 360, -> (implies) wi 4, -. (not) wn 3, <-> (logical equivalence) df-bi 178, -/\ (nand aka Sheffer stroke) df-nan 1297, and \/_ (exclusive or) df-xor 1314.
Theorem	truantru 1345	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. /\ T. ) <-> T. )
Theorem	truanfal 1346	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. /\ F. ) <-> F. )
Theorem	falantru 1347	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. /\ T. ) <-> F. )
Theorem	falanfal 1348	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. /\ F. ) <-> F. )
Theorem	truortru 1349	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. \/ T. ) <-> T. )
Theorem	truorfal 1350	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. \/ F. ) <-> T. )
Theorem	falortru 1351	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. \/ T. ) <-> T. )
Theorem	falorfal 1352	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. \/ F. ) <-> F. )
Theorem	truimtru 1353	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. -> T. ) <-> T. )
Theorem	truimfal 1354	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -> F. ) <-> F. )
Theorem	falimtru 1355	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. -> T. ) <-> T. )
Theorem	falimfal 1356	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. -> F. ) <-> T. )
Theorem	nottru 1357	A -. identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( -. T. <-> F. )
Theorem	notfal 1358	A -. identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( -. F. <-> T. )
Theorem	trubitru 1359	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. <-> T. ) <-> T. )
Theorem	trubifal 1360	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. <-> F. ) <-> F. )
Theorem	falbitru 1361	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. <-> T. ) <-> F. )
Theorem	falbifal 1362	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. <-> F. ) <-> T. )
Theorem	trunantru 1363	A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -/\ T. ) <-> F. )
Theorem	trunanfal 1364	A -/\ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -/\ F. ) <-> T. )
Theorem	falnantru 1365	A -/\ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. -/\ T. ) <-> T. )
Theorem	falnanfal 1366	A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. -/\ F. ) <-> T. )
Theorem	truxortru 1367	A \/_ identity. (Contributed by David A. Wheeler, 8-May-2015.)
|- ( ( T. \/_ T. ) <-> F. )
Theorem	truxorfal 1368	A \/_ identity. (Contributed by David A. Wheeler, 8-May-2015.)
|- ( ( T. \/_ F. ) <-> T. )
Theorem	falxortru 1369	A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015.)
|- ( ( F. \/_ T. ) <-> T. )
Theorem	falxorfal 1370	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 1371	Virtual deduction rule e22 28772 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 1372	e12an 28837 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 1373	e23 28867 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 1374	Exportation implication also converting head from biconditional to conditional. This proof is exbirVD 28965 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 1375	impexp 434 with a 3-conjunct antecedent. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( ( ( ph /\ ps /\ ch ) -> th ) <-> ( ph -> ( ps -> ( ch -> th ) ) ) )
Theorem	3impexpbicom 1376	3impexp 1375 with biconditional consequent of antecedent that is commuted in consequent. Derived automatically from 3impexpVD 28968. (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 1377	Deduction form of 3impexpbicom 1376. Derived automatically from 3impexpbicomiVD 28970. (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 1378	Closed form of ancoms 440. Derived automatically from ancomsimpVD 28977. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( ( ( ph /\ ps ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )
Theorem	exp3acom3r 1379	Export and commute antecedents. (Contributed by Alan Sare, 18-Mar-2012.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ps -> ( ch -> ( ph -> th ) ) )
Theorem	exp3acom23g 1380	Implication form of exp3acom23 1381. (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 1381	The exportation deduction exp3a 426 with commutation of the conjoined wwfs. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> ( ch -> ( ps -> th ) ) )
Theorem	simplbi2comg 1382	Implication form of simplbi2com 1383. (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 1383	A deduction eliminating a conjunct, similar to simplbi2 609. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ps -> ph ) )
Theorem	ee21 1384	e21 28842 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 1385	e10 28795 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 1386	e02 28798 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 1387	Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.)
wff hadd ( ph , ps , ch )
Syntax	wcad 1388	Define the half adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
wff cadd ( ph , ps , ch )
Definition	df-had 1389	Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )
Definition	df-cad 1390	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 1391	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 1392	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 1393	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 1394	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 1395	Associative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )
Theorem	hadbi 1396	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 1397	Commutative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ps , ph , ch ) )
Theorem	hadcomb 1398	Commutative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ph , ch , ps ) )
Theorem	hadrot 1399	Rotation law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ps , ch , ph ) )
Theorem	cador 1400	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 ) ) )