![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl5breqr | Structured version Visualization version GIF version |
Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
Ref | Expression |
---|---|
syl5breqr.1 | ⊢ 𝐴𝑅𝐵 |
syl5breqr.2 | ⊢ (𝜑 → 𝐶 = 𝐵) |
Ref | Expression |
---|---|
syl5breqr | ⊢ (𝜑 → 𝐴𝑅𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5breqr.1 | . 2 ⊢ 𝐴𝑅𝐵 | |
2 | syl5breqr.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐵) | |
3 | 2 | eqcomd 2657 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | syl5breq 4722 | 1 ⊢ (𝜑 → 𝐴𝑅𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 class class class wbr 4685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 |
This theorem is referenced by: r1sdom 8675 alephordilem1 8934 mulge0 10584 xsubge0 12129 xmulgt0 12151 xmulge0 12152 xlemul1a 12156 sqlecan 13011 bernneq 13030 hashge1 13216 hashge2el2dif 13300 cnpart 14024 sqr0lem 14025 bitsfzo 15204 bitsmod 15205 bitsinv1lem 15210 pcge0 15613 prmreclem4 15670 prmreclem5 15671 isabvd 18868 abvtrivd 18888 isnzr2hash 19312 nmolb2d 22569 nmoi 22579 nmoleub 22582 nmo0 22586 ovolge0 23295 itg1ge0a 23523 fta1g 23972 plyrem 24105 taylfval 24158 abelthlem2 24231 sinq12ge0 24305 relogrn 24353 logneg 24379 cxpge0 24474 amgmlem 24761 bposlem5 25058 lgsdir2lem2 25096 2lgsoddprmlem3 25184 rpvmasumlem 25221 eupth2lem3lem3 27208 eupth2lemb 27215 blocnilem 27787 pjssge0ii 28669 unierri 29091 xlt2addrd 29651 locfinref 30036 esumcst 30253 ballotlem5 30689 poimirlem23 33562 poimirlem25 33564 poimirlem26 33565 poimirlem27 33566 poimirlem28 33567 itgaddnclem2 33599 pell14qrgt0 37740 monotoddzzfi 37824 rmxypos 37831 rmygeid 37848 stoweidlem18 40553 stoweidlem55 40590 wallispi2lem1 40606 fourierdlem62 40703 fourierdlem103 40744 fourierdlem104 40745 fourierswlem 40765 pgrpgt2nabl 42472 pw2m1lepw2m1 42635 amgmwlem 42876 |
Copyright terms: Public domain | W3C validator |