Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqbrtrdi | Structured version Visualization version GIF version |
Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
Ref | Expression |
---|---|
eqbrtrdi.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqbrtrdi.2 | ⊢ 𝐵𝑅𝐶 |
Ref | Expression |
---|---|
eqbrtrdi | ⊢ (𝜑 → 𝐴𝑅𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqbrtrdi.2 | . 2 ⊢ 𝐵𝑅𝐶 | |
2 | eqbrtrdi.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 2 | breq1d 5063 | . 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
4 | 1, 3 | mpbiri 261 | 1 ⊢ (𝜑 → 𝐴𝑅𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 class class class wbr 5053 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 |
This theorem is referenced by: eqbrtrrdi 5093 domunsn 8796 mapdom1 8811 mapdom2 8817 pm54.43 9617 infmap2 9832 inar1 10389 gruina 10432 nn0ledivnn 12699 xltnegi 12806 leexp1a 13745 discr 13807 facwordi 13855 faclbnd3 13858 hashgt12el 13989 hashle2pr 14043 cnpart 14803 geomulcvg 15440 dvds1 15880 ramz2 16577 ramz 16578 gex1 18980 sylow2a 19008 en1top 21881 en2top 21882 hmph0 22692 ptcmplem2 22950 dscmet 23470 dscopn 23471 xrge0tsms2 23732 htpycc 23877 pcohtpylem 23916 pcopt 23919 pcopt2 23920 pcoass 23921 pcorevlem 23923 vitalilem5 24509 dvef 24877 dveq0 24897 dv11cn 24898 deg1lt0 24989 ply1rem 25061 fta1g 25065 plyremlem 25197 aalioulem3 25227 pige3ALT 25409 relogrn 25450 logneg 25476 cxpaddlelem 25637 mule1 26030 ppiub 26085 dchrabs2 26143 bposlem1 26165 zabsle1 26177 lgseisen 26260 lgsquadlem2 26262 rpvmasumlem 26368 qabvle 26506 ostth3 26519 colinearalg 27001 eengstr 27071 clwwlknon1le1 28184 eucrct2eupth 28328 nmosetn0 28846 nmoo0 28872 siii 28934 bcsiALT 29260 branmfn 30186 esumrnmpt2 31748 ballotlemrc 32209 pthhashvtx 32802 subfacval3 32864 sconnpi1 32914 fz0n 33414 poimirlem31 35545 itg2addnclem 35565 ftc1anc 35595 radcnvrat 41608 infxr 42582 stoweidlem18 43237 stoweidlem55 43274 fourierdlem62 43387 fourierswlem 43449 exple2lt6 45376 fvconstdomi 45863 f1omoALT 45865 indthincALT 46010 |
Copyright terms: Public domain | W3C validator |