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 2085 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | syl6req 2130 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1284 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-4 1440 ax-17 1459 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-cleq 2074 |
This theorem is referenced by: iftrue 3356 iffalse 3359 difprsn1 3525 dmmptg 4838 relcoi1 4869 funimacnv 4995 dffv3g 5194 dfimafn 5243 fvco2 5263 isoini 5477 oprabco 5858 supval2ti 6408 eqneg 7820 zeo 8452 fseq1p1m1 9111 iseqval 9440 mulgcd 10405 ialgrp1 10428 ialgcvg 10430 |
Copyright terms: Public domain | W3C validator |