![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addcomli | Unicode version |
Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
mul.1 |
![]() ![]() ![]() ![]() |
mul.2 |
![]() ![]() ![]() ![]() |
addcomli.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
addcomli |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mul.2 |
. . 3
![]() ![]() ![]() ![]() | |
2 | mul.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | addcomi 8104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | addcomli.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtri 2198 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 ax-addcom 7914 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: negsubdi2i 8246 1p2e3 9056 peano2z 9292 4t4e16 9485 6t3e18 9491 6t5e30 9493 7t3e21 9496 7t4e28 9497 7t6e42 9499 7t7e49 9500 8t3e24 9502 8t4e32 9503 8t5e40 9504 8t8e64 9507 9t3e27 9509 9t4e36 9510 9t5e45 9511 9t6e54 9512 9t7e63 9513 9t8e72 9514 9t9e81 9515 4bc3eq4 10756 n2dvdsm1 11921 6gcd4e2 11999 eulerid 14384 cosq23lt0 14415 binom4 14558 lgsdir2lem1 14590 m1lgs 14613 2lgsoddprmlem3d 14619 ex-exp 14640 ex-bc 14642 ex-gcd 14644 |
Copyright terms: Public domain | W3C validator |