| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > eqtr2id | Unicode version | ||
| Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
| Ref | Expression |
|---|---|
| eqtr2id.1 |
|
| eqtr2id.2 |
|
| Ref | Expression |
|---|---|
| eqtr2id |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqtr2id.1 |
. . 3
| |
| 2 | eqtr2id.2 |
. . 3
| |
| 3 | 1, 2 | eqtrid 2249 |
. 2
|
| 4 | 3 | eqcomd 2210 |
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 1469 ax-gen 1471 ax-4 1532 ax-17 1548 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-cleq 2197 |
| This theorem is referenced by: eqtr3di 2252 opeqsn 4296 dcextest 4628 relop 4827 funopg 5304 funcnvres 5346 mapsnconst 6780 snexxph 7051 apreap 8659 recextlem1 8723 nn0supp 9346 intqfrac2 10462 hashprg 10951 hashfacen 10979 ccatrid 11061 explecnv 11787 grp1inv 13410 rnrhmsubrg 13985 rerestcntop 15001 rerest 15003 mpomulcn 15009 binom4 15422 |
| Copyright terms: Public domain | W3C validator |