![]() |
Metamath
Proof Explorer Theorem List (p. 14 of 325) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | ![]() (1-22382) |
![]() (22383-23905) |
![]() (23906-32459) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nanbi1 1301 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi2 1302 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi12 1303 | Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi1i 1304 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi2i 1305 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi12i 1306 | Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi1d 1307 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi2d 1308 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nanbi12d 1309 | Join two logical equivalences with anti-conjunction. (Contributed by Scott Fenton, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wxo 1310 | Extend wff definition to include exclusive disjunction ('xor'). |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-xor 1311 |
Define exclusive disjunction (logical 'xor'). Return true if either the
left or right, but not both, are true. After we define the constant true
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xnor 1312 | Two ways to write XNOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xorcom 1313 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xorass 1314 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | excxor 1315 | This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xor2 1316 | Two ways to express "exclusive or." (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xorneg1 1317 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xorneg2 1318 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xorneg 1319 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xorbi12i 1320 | Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xorbi12d 1321 | Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wtru 1322 |
![]() |
![]() ![]() | ||
Syntax | wfal 1323 |
![]() |
![]() ![]() | ||
Theorem | trujust 1324 | Soundness justification theorem for df-tru 1325. (Contributed by Mario Carneiro, 17-Nov-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-tru 1325 |
Definition of ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-fal 1326 |
Definition of ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | tru 1327 |
![]() |
![]() ![]() | ||
Theorem | fal 1328 |
![]() |
![]() ![]() ![]() | ||
Theorem | trud 1329 |
Eliminate ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | tbtru 1330 |
If something is true, it outputs ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nbfal 1331 |
If something is not true, it outputs ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bitru 1332 | A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bifal 1333 | A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falim 1334 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falimd 1335 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | a1tru 1336 |
Anything implies ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truan 1337 | True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dfnot 1338 |
Given falsum, we can define the negation of a wff ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | inegd 1339 | Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | efald 1340 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pm2.21fal 1341 | If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
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 ( | ||
Theorem | truantru 1342 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truanfal 1343 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falantru 1344 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falanfal 1345 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truortru 1346 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truorfal 1347 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falortru 1348 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falorfal 1349 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truimtru 1350 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truimfal 1351 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falimtru 1352 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falimfal 1353 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nottru 1354 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | notfal 1355 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | trubitru 1356 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | trubifal 1357 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falbitru 1358 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falbifal 1359 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | trunantru 1360 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | trunanfal 1361 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falnantru 1362 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falnanfal 1363 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truxortru 1364 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truxorfal 1365 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falxortru 1366 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | falxorfal 1367 |
A ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ee22 1368 | Virtual deduction rule e22 28490 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. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ee12an 1369 | e12an 28555 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. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ee23 1370 | e23 28585 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exbir 1371 | Exportation implication also converting head from biconditional to conditional. This proof is exbirVD 28683 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3impexp 1372 | impexp 434 with a 3-conjunct antecedent. (Contributed by Alan Sare, 31-Dec-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3impexpbicom 1373 | 3impexp 1372 with biconditional consequent of antecedent that is commuted in consequent. Derived automatically from 3impexpVD 28686. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3impexpbicomi 1374 | Deduction form of 3impexpbicom 1373. Derived automatically from 3impexpbicomiVD 28688. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ancomsimp 1375 | Closed form of ancoms 440. Derived automatically from ancomsimpVD 28695. (Contributed by Alan Sare, 31-Dec-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exp3acom3r 1376 | Export and commute antecedents. (Contributed by Alan Sare, 18-Mar-2012.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exp3acom23g 1377 | Implication form of exp3acom23 1378. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exp3acom23 1378 | The exportation deduction exp3a 426 with commutation of the conjoined wwfs. (Contributed by Alan Sare, 22-Jul-2012.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | simplbi2comg 1379 | Implication form of simplbi2com 1380. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | simplbi2com 1380 | A deduction eliminating a conjunct, similar to simplbi2 609. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ee21 1381 | e21 28560 without virtual deductions. (Contributed by Alan Sare, 18-Mar-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ee10 1382 | e10 28513 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) TODO: this is frequently used; come up with better label. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ee02 1383 | e02 28516 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) TODO: decide if this is worth keeping. |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
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 1384 | Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wcad 1385 | Define the half adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-had 1386 | Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-cad 1387 | Define the half adder carry, which is true when at least two arguments are true. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadbi123d 1388 | Equality theorem for half adder. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cadbi123d 1389 | Equality theorem for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadbi123i 1390 | Equality theorem for half adder. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cadbi123i 1391 | Equality theorem for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadass 1392 | Associative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadbi 1393 | The half adder is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadcoma 1394 | Commutative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadcomb 1395 | Commutative law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadrot 1396 | Rotation law for triple XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cador 1397 | Write the adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cadan 1398 | Write the adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hadnot 1399 | The half adder distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cadnot 1400 | The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |