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 | syl5eq 2202 | . 2 |
4 | 3 | eqcomd 2163 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1335 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 ax-4 1490 ax-17 1506 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 |
This theorem is referenced by: eqtr3di 2205 opeqsn 4215 dcextest 4543 relop 4739 funopg 5207 funcnvres 5246 mapsnconst 6642 snexxph 6897 apreap 8467 recextlem1 8530 nn0supp 9148 intqfrac2 10228 hashprg 10694 hashfacen 10719 explecnv 11414 rerestcntop 13046 binom4 13393 |
Copyright terms: Public domain | W3C validator |