| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > breqtrrid | Structured version Visualization version GIF version | ||
| Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
| Ref | Expression |
|---|---|
| breqtrrid.1 | ⊢ 𝐴𝑅𝐵 |
| breqtrrid.2 | ⊢ (𝜑 → 𝐶 = 𝐵) |
| Ref | Expression |
|---|---|
| breqtrrid | ⊢ (𝜑 → 𝐴𝑅𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breqtrrid.1 | . 2 ⊢ 𝐴𝑅𝐵 | |
| 2 | breqtrrid.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐵) | |
| 3 | 2 | eqcomd 2743 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
| 4 | 1, 3 | breqtrid 5180 | 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: r1sdom 9814 alephordilem1 10113 mulge0 11781 xsubge0 13303 xmulgt0 13325 xmulge0 13326 xlemul1a 13330 sqlecan 14248 bernneq 14268 hashge1 14428 hashge2el2dif 14519 cnpart 15279 sqrt0 15280 bitsfzo 16472 bitsmod 16473 bitsinv1lem 16478 pcge0 16900 prmreclem4 16957 prmreclem5 16958 isnzr2hash 20519 isabvd 20813 abvtrivd 20833 nmolb2d 24739 nmoi 24749 nmoleub 24752 nmo0 24756 ovolge0 25516 itg1ge0a 25746 fta1g 26209 plyrem 26347 taylfval 26400 abelthlem2 26476 sinq12ge0 26550 relogrn 26603 logneg 26630 cxpge0 26725 amgmlem 27033 bposlem5 27332 lgsdir2lem2 27370 2lgsoddprmlem3 27458 rpvmasumlem 27531 mulsge0d 28172 expsgt0 28415 eupth2lem3lem3 30249 eupth2lemb 30256 blocnilem 30823 pjssge0ii 31701 unierri 32123 xlt2addrd 32762 2sqr3minply 33791 locfinref 33840 esumcst 34064 ballotlem5 34502 poimirlem23 37650 poimirlem25 37652 poimirlem26 37653 poimirlem27 37654 poimirlem28 37655 itgaddnclem2 37686 pell14qrgt0 42870 monotoddzzfi 42954 rmxypos 42959 rmygeid 42976 stoweidlem18 46033 stoweidlem55 46070 wallispi2lem1 46086 fourierdlem62 46183 fourierdlem103 46224 fourierdlem104 46225 fourierswlem 46245 2ltceilhalf 48015 pgrpgt2nabl 48282 pw2m1lepw2m1 48437 amgmwlem 49321 |
| Copyright terms: Public domain | W3C validator |