![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3brtr3d | GIF version |
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.) |
Ref | Expression |
---|---|
3brtr3d.1 | ⊢ (𝜑 → 𝐴𝑅𝐵) |
3brtr3d.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3brtr3d.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3brtr3d | ⊢ (𝜑 → 𝐶𝑅𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3brtr3d.1 | . 2 ⊢ (𝜑 → 𝐴𝑅𝐵) | |
2 | 3brtr3d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐶) | |
3 | 3brtr3d.3 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐷) | |
4 | 2, 3 | breq12d 4013 | . 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷)) |
5 | 1, 4 | mpbid 147 | 1 ⊢ (𝜑 → 𝐶𝑅𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 class class class wbr 4000 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-un 3133 df-sn 3597 df-pr 3598 df-op 3600 df-br 4001 |
This theorem is referenced by: ofrval 6086 phplem2 6846 ltaddnq 7384 prarloclemarch2 7396 prmuloclemcalc 7542 axcaucvglemcau 7875 apreap 8521 ltmul1 8526 divap1d 8734 div2subap 8770 lemul2a 8792 mul2lt0rlt0 9733 xleadd2a 9848 monoord2 10450 expubnd 10550 bernneq2 10614 nn0ltexp2 10661 apexp1 10669 resqrexlemcalc2 10995 resqrexlemcalc3 10996 abs2dif2 11087 bdtrilem 11218 bdtri 11219 xrmaxaddlem 11239 fsum00 11441 iserabs 11454 geosergap 11485 mertenslemi1 11514 eftlub 11669 eirraplem 11755 unitmulcl 13094 unitgrp 13097 xblss2 13538 xmstri2 13603 mstri2 13604 xmstri 13605 mstri 13606 xmstri3 13607 mstri3 13608 msrtri 13609 logdivlti 13935 2sqlem8 14092 apdifflemr 14418 |
Copyright terms: Public domain | W3C validator |