Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6reqr | GIF 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 2121 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | syl6req 2167 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: iftrue 3449 iffalse 3452 difprsn1 3629 dmmptg 5006 relcoi1 5040 funimacnv 5169 dmmptd 5223 dffv3g 5385 dfimafn 5438 fvco2 5458 isoini 5687 oprabco 6082 ixpconstg 6569 unfiexmid 6774 undifdc 6780 sbthlemi4 6816 sbthlemi5 6817 sbthlemi6 6818 supval2ti 6850 exmidfodomrlemim 7025 suplocexprlemex 7498 eqneg 8460 zeo 9124 fseq1p1m1 9842 seq3val 10199 seqvalcd 10200 hashfzo 10536 hashxp 10540 fsumconst 11191 modfsummod 11195 telfsumo 11203 mulgcd 11631 algcvg 11656 phiprmpw 11825 strslfv3 11931 uptx 12370 resubmet 12644 |
Copyright terms: Public domain | W3C validator |