Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6reqr | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
syl6reqr.1 | |
syl6reqr.2 |
Ref | Expression |
---|---|
syl6reqr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6reqr.1 | . 2 | |
2 | syl6reqr.2 | . . 3 | |
3 | 2 | eqcomi 2044 | . 2 |
4 | 1, 3 | syl6req 2089 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1243 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: iftrue 3336 iffalse 3339 difprsn1 3503 dmmptg 4818 relcoi1 4849 funimacnv 4975 dffv3g 5174 dfimafn 5222 fvco2 5242 isoini 5457 oprabco 5838 eqneg 7708 zeo 8343 fseq1p1m1 8956 iseqval 9220 ialgrp1 9885 ialgcvg 9887 |
Copyright terms: Public domain | W3C validator |