| 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 2218 |
. 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 1470 ax-gen 1472 ax-4 1533 ax-17 1549 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-cleq 2198 |
| This theorem is referenced by: eqeqan12rd 2222 eqfnfv 5677 eqfnfv2 5678 f1mpt 5840 xpopth 6262 f1o2ndf1 6314 ecopoveq 6717 xpdom2 6926 djune 7180 addpipqqs 7483 enq0enq 7544 enq0sym 7545 enq0tr 7547 enq0breq 7549 preqlu 7585 cnegexlem1 8247 neg11 8323 subeqrev 8448 cnref1o 9772 xneg11 9956 modlteq 10542 sq11 10757 qsqeqor 10795 fz1eqb 10935 eqwrd 11034 s111 11085 cj11 11216 sqrt11 11350 sqabs 11393 recan 11420 reeff1 12011 efieq 12046 xpsff1o 13181 ismhm 13293 isdomn 14031 tgtop11 14548 ioocosf1o 15326 mpodvdsmulf1o 15462 |
| Copyright terms: Public domain | W3C validator |