![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl6eqbr | Structured version Visualization version GIF version |
Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
Ref | Expression |
---|---|
syl6eqbr.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
syl6eqbr.2 | ⊢ 𝐵𝑅𝐶 |
Ref | Expression |
---|---|
syl6eqbr | ⊢ (𝜑 → 𝐴𝑅𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6eqbr.2 | . 2 ⊢ 𝐵𝑅𝐶 | |
2 | syl6eqbr.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 2 | breq1d 4814 | . 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
4 | 1, 3 | mpbiri 248 | 1 ⊢ (𝜑 → 𝐴𝑅𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 class class class wbr 4804 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-br 4805 |
This theorem is referenced by: syl6eqbrr 4844 domunsn 8277 mapdom1 8292 mapdom2 8298 pm54.43 9036 cdadom1 9220 infmap2 9252 inar1 9809 gruina 9852 nn0ledivnn 12154 xltnegi 12260 leexp1a 13133 discr 13215 facwordi 13290 faclbnd3 13293 hashgt12el 13422 hashle2pr 13471 cnpart 14199 geomulcvg 14826 dvds1 15263 ramz2 15950 ramz 15951 gex1 18226 sylow2a 18254 en1top 21010 en2top 21011 hmph0 21820 ptcmplem2 22078 dscmet 22598 dscopn 22599 xrge0tsms2 22859 htpycc 23000 pcohtpylem 23039 pcopt 23042 pcopt2 23043 pcoass 23044 pcorevlem 23046 vitalilem5 23600 dvef 23962 dveq0 23982 dv11cn 23983 deg1lt0 24070 ply1rem 24142 fta1g 24146 plyremlem 24278 aalioulem3 24308 pige3 24489 relogrn 24528 logneg 24554 cxpaddlelem 24712 mule1 25094 ppiub 25149 dchrabs2 25207 bposlem1 25229 zabsle1 25241 lgseisen 25324 lgsquadlem2 25326 rpvmasumlem 25396 qabvle 25534 ostth3 25547 colinearalg 26010 eengstr 26080 clwwlknon1le1 27270 eucrct2eupth 27418 nmosetn0 27950 nmoo0 27976 siii 28038 bcsiALT 28366 branmfn 29294 esumrnmpt2 30460 ballotlemrc 30922 subfacval3 31499 sconnpi1 31549 fz0n 31944 poimirlem31 33771 itg2addnclem 33792 ftc1anc 33824 radcnvrat 39033 infxr 40099 stoweidlem18 40756 stoweidlem55 40793 fourierdlem62 40906 fourierswlem 40968 exple2lt6 42673 |
Copyright terms: Public domain | W3C validator |