| 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 5153 | . 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
| 4 | 1, 3 | mpbiri 258 | 1 ⊢ (𝜑 → 𝐴𝑅𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 class class class wbr 5143 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 |
| This theorem is referenced by: eqbrtrrdi 5183 domunsn 9167 mapdom1 9182 mapdom2 9188 pm54.43 10041 infmap2 10257 inar1 10815 gruina 10858 nn0ledivnn 13148 xltnegi 13258 leexp1a 14215 discr 14279 facwordi 14328 faclbnd3 14331 hashgt12el 14461 hashle2pr 14516 cnpart 15279 geomulcvg 15912 dvds1 16356 ramz2 17062 ramz 17063 gex1 19609 sylow2a 19637 en1top 22991 en2top 22992 hmph0 23803 ptcmplem2 24061 dscmet 24585 dscopn 24586 xrge0tsms2 24857 htpycc 25012 pcohtpylem 25052 pcopt 25055 pcopt2 25056 pcoass 25057 pcorevlem 25059 vitalilem5 25647 dvef 26018 dveq0 26039 dv11cn 26040 deg1lt0 26130 ply1rem 26205 fta1g 26209 plyremlem 26346 aalioulem3 26376 pige3ALT 26562 relogrn 26603 logneg 26630 cxpaddlelem 26794 mule1 27191 ppiub 27248 dchrabs2 27306 bposlem1 27328 zabsle1 27340 lgseisen 27423 lgsquadlem2 27425 rpvmasumlem 27531 qabvle 27669 ostth3 27682 precsexlem9 28239 nnsrecgt0d 28356 cutpw2 28417 pw2bday 28418 0reno 28429 colinearalg 28925 eengstr 28995 clwwlknon1le1 30120 eucrct2eupth 30264 nmosetn0 30784 nmoo0 30810 siii 30872 bcsiALT 31198 branmfn 32124 fzo0opth 32807 drngidlhash 33462 m1pmeq 33608 esumrnmpt2 34069 ballotlemrc 34533 pthhashvtx 35133 subfacval3 35194 sconnpi1 35244 fz0n 35731 poimirlem31 37658 itg2addnclem 37678 ftc1anc 37708 safesnsupfidom1o 43430 radcnvrat 44333 infxr 45378 stoweidlem18 46033 stoweidlem55 46070 fourierdlem62 46183 fourierswlem 46245 exple2lt6 48280 fvconstdomi 48791 f1omoALT 48793 indthincALT 49110 |
| Copyright terms: Public domain | W3C validator |