![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1p2e3 | Structured version Visualization version Unicode version |
Description: 1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
1p2e3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 10687 |
. 2
![]() ![]() ![]() ![]() | |
2 | ax-1cn 9602 |
. 2
![]() ![]() ![]() ![]() | |
3 | 2p1e3 10740 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | addcomli 9830 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-mpt 4466 df-id 4752 df-po 4758 df-so 4759 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-ov 6298 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-pnf 9682 df-mnf 9683 df-ltxr 9685 df-2 10675 df-3 10676 |
This theorem is referenced by: binom3 12400 3lcm2e6woprm 14592 prmgaplem7 15039 2exp16 15073 prmlem1a 15090 23prm 15102 prmlem2 15103 83prm 15106 163prm 15108 317prm 15109 631prm 15110 1259lem3 15116 1259lem4 15117 1259prm 15119 2503lem2 15121 2503lem3 15122 4001lem2 15125 quart1lem 23793 log2ublem3 23886 log2ub 23887 pntibndlem2 24441 1kp2ke3k 25908 ex-ind-dvds 25911 fib4 29249 rabren3dioph 35670 nnsum4primesodd 38901 nnsum4primesoddALTV 38902 |
Copyright terms: Public domain | W3C validator |