Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqtr3id | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtr3id.1 | ⊢ 𝐵 = 𝐴 |
eqtr3id.2 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
eqtr3id | ⊢ (𝜑 → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr3id.1 | . . 3 ⊢ 𝐵 = 𝐴 | |
2 | 1 | eqcomi 2168 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqtr3id.2 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
4 | 2, 3 | syl5eq 2209 | 1 ⊢ (𝜑 → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: 3eqtr3g 2220 csbeq1a 3052 ssdifeq0 3489 pofun 4287 opabbi2dv 4750 funimaexg 5269 fresin 5363 f1imacnv 5446 foimacnv 5447 fsn2 5656 fmptpr 5674 funiunfvdm 5728 funiunfvdmf 5729 fcof1o 5754 f1opw2 6041 fnexALT 6076 eqerlem 6526 pmresg 6636 mapsn 6650 fopwdom 6796 mapen 6806 fiintim 6888 xpfi 6889 sbthlemi8 6923 sbthlemi9 6924 ctssdccl 7070 exmidfodomrlemim 7151 mul02 8279 recdivap 8608 fzpreddisj 10000 fzshftral 10037 qbtwnrelemcalc 10185 frec2uzrdg 10338 frecuzrdgrcl 10339 frecuzrdgsuc 10343 frecuzrdgrclt 10344 frecuzrdgg 10345 binom3 10566 bcn2 10671 hashfz1 10690 hashunlem 10711 hashfacen 10743 cnrecnv 10846 resqrexlemnm 10954 amgm2 11054 2zsupmax 11161 xrmaxltsup 11193 xrmaxadd 11196 xrbdtri 11211 fisumss 11327 fsumcnv 11372 telfsumo 11401 fsumiun 11412 arisum2 11434 fprodssdc 11525 fprodsplitdc 11531 fprodsplit 11532 fprodcnv 11560 ege2le3 11606 efgt1p 11631 cos01bnd 11693 suprzubdc 11879 dfgcd3 11937 eucalgval 11980 sqrt2irrlem 12087 pcid 12249 setsslid 12438 baspartn 12646 txdis1cn 12876 cnmpt21 12889 cnmpt22 12892 hmeores 12913 metreslem 12978 remetdval 13137 dvfvalap 13248 binom4 13495 nninfsellemqall 13788 |
Copyright terms: Public domain | W3C validator |