![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeqan12d | Unicode version |
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
eqeqan12d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eqeqan12d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqeqan12d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeqan12d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqeqan12d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqeq12 2190 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2an 289 |
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 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: eqeqan12rd 2194 eqfnfv 5613 eqfnfv2 5614 f1mpt 5771 xpopth 6176 f1o2ndf1 6228 ecopoveq 6629 xpdom2 6830 djune 7076 addpipqqs 7368 enq0enq 7429 enq0sym 7430 enq0tr 7432 enq0breq 7434 preqlu 7470 cnegexlem1 8131 neg11 8207 subeqrev 8332 cnref1o 9649 xneg11 9833 modlteq 10396 sq11 10592 qsqeqor 10630 fz1eqb 10769 cj11 10913 sqrt11 11047 sqabs 11090 recan 11117 reeff1 11707 efieq 11742 xpsff1o 12767 ismhm 12852 tgtop11 13546 ioocosf1o 14245 |
Copyright terms: Public domain | W3C validator |