![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3brtr4d | GIF version |
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.) |
Ref | Expression |
---|---|
3brtr4d.1 | ⊢ (𝜑 → 𝐴𝑅𝐵) |
3brtr4d.2 | ⊢ (𝜑 → 𝐶 = 𝐴) |
3brtr4d.3 | ⊢ (𝜑 → 𝐷 = 𝐵) |
Ref | Expression |
---|---|
3brtr4d | ⊢ (𝜑 → 𝐶𝑅𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3brtr4d.1 | . 2 ⊢ (𝜑 → 𝐴𝑅𝐵) | |
2 | 3brtr4d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐴) | |
3 | 3brtr4d.3 | . . 3 ⊢ (𝜑 → 𝐷 = 𝐵) | |
4 | 2, 3 | breq12d 3880 | . 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵)) |
5 | 1, 4 | mpbird 166 | 1 ⊢ (𝜑 → 𝐶𝑅𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1296 class class class wbr 3867 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-un 3017 df-sn 3472 df-pr 3473 df-op 3475 df-br 3868 |
This theorem is referenced by: f1oiso2 5644 prarloclemarch2 7075 caucvgprprlemmu 7351 caucvgsrlembound 7436 mulap0 8220 lediv12a 8452 recp1lt1 8457 xleadd1a 9439 fldiv4p1lem1div2 9861 intfracq 9876 modqmulnn 9898 addmodlteq 9954 frecfzennn 9982 monoord2 10027 expgt1 10108 leexp2r 10124 leexp1a 10125 bernneq 10189 faclbnd 10264 faclbnd6 10267 facubnd 10268 hashunlem 10327 zfz1isolemiso 10359 sqrtgt0 10582 absrele 10631 absimle 10632 abstri 10652 abs2difabs 10656 bdtrilem 10785 bdtri 10786 xrmaxifle 10789 xrmaxadd 10804 xrbdtri 10819 climsqz 10878 climsqz2 10879 fsum3cvg2 10937 isumle 11038 expcnvap0 11045 expcnvre 11046 explecnv 11048 cvgratz 11075 efcllemp 11097 ege2le3 11110 eflegeo 11141 phibnd 11620 psmetres2 12119 xmetres2 12165 comet 12285 bdxmet 12287 cnmet 12309 |
Copyright terms: Public domain | W3C validator |