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 2616 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | syl5breq 4620 | 1 ⊢ (𝜑 → 𝐴𝑅𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 class class class wbr 4583 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 |
This theorem is referenced by: r1sdom 8520 alephordilem1 8779 mulge0 10425 xsubge0 11963 xmulgt0 11985 xmulge0 11986 xlemul1a 11990 sqlecan 12833 bernneq 12852 hashge1 13039 hashge2el2dif 13117 cnpart 13828 sqr0lem 13829 bitsfzo 14995 bitsmod 14996 bitsinv1lem 15001 pcge0 15404 prmreclem4 15461 prmreclem5 15462 isabvd 18643 abvtrivd 18663 isnzr2hash 19085 nmolb2d 22332 nmoi 22342 nmoleub 22345 nmo0 22349 ovolge0 23056 itg1ge0a 23284 fta1g 23731 plyrem 23864 taylfval 23917 abelthlem2 23990 sinq12ge0 24064 relogrn 24112 logneg 24138 cxpge0 24229 amgmlem 24516 bposlem5 24813 lgsdir2lem2 24851 2lgsoddprmlem3 24939 rpvmasumlem 24976 eupath2lem3 26506 eupath2 26507 frgrawopreglem2 26572 blocnilem 27043 pjssge0ii 27925 unierri 28347 xlt2addrd 28913 locfinref 29236 esumcst 29452 ballotlem5 29888 poimirlem23 32602 poimirlem25 32604 poimirlem26 32605 poimirlem27 32606 poimirlem28 32607 itgaddnclem2 32639 pell14qrgt0 36441 monotoddzzfi 36525 rmxypos 36532 rmygeid 36549 stoweidlem18 38911 stoweidlem55 38948 wallispi2lem1 38964 fourierdlem62 39061 fourierdlem103 39102 fourierdlem104 39103 fourierswlem 39123 eupth2lem3lem3 41398 eupth2lemb 41405 pgrpgt2nabl 41941 pw2m1lepw2m1 42104 amgmwlem 42357 |
Copyright terms: Public domain | W3C validator |