![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equequ1 | Structured version Visualization version GIF version |
Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.) |
Ref | Expression |
---|---|
equequ1 | ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax7 2019 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | |
2 | equtr 2024 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧)) | |
3 | 1, 2 | impbid 211 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 |
This theorem is referenced by: equvinv 2032 equvelv 2034 spaev 2055 sbjust 2066 equsb3 2101 sbievg 2360 drsb1 2498 mo4 2565 sb8eulem 2597 cbvmovw 2601 cbvmow 2602 axextg 2710 reu6 3682 reu7 3688 reu8nf 3831 disjxun 5101 solin 5568 cbviotaw 6452 cbviota 6455 dff13f 7199 poxp 8052 poxp2 8067 poxp3 8074 unxpdomlem1 9152 unxpdomlem2 9153 aceq0 10012 zfac 10354 axrepndlem1 10486 zfcndac 10513 injresinj 13647 fsum2dlem 15615 ramub1lem2 16859 ramcl 16861 symgextf1 19162 mamulid 21742 mamurid 21743 mdetdiagid 21901 mdetunilem9 21921 alexsubALTlem3 23352 ptcmplem2 23356 dscmet 23880 dyadmbllem 24915 opnmbllem 24917 isppw2 26416 2sqreulem1 26746 2sqreunnlem1 26749 frgr2wwlk1 29102 disji2f 31324 disjif2 31328 bj-ssblem1 35056 bj-ssblem2 35057 cbveud 35781 wl-naevhba1v 35917 wl-equsb3 35949 mblfinlem1 36053 bfp 36221 dveeq1-o 37335 dveeq1-o16 37336 axc11n-16 37338 ax12eq 37341 fsuppind 40674 mhphf 40680 fphpd 41048 ax6e2nd 42751 ax6e2ndVD 43101 ax6e2ndALT 43123 disjinfi 43317 iundjiun 44602 hspdifhsp 44758 hspmbl 44771 2reu8i 45246 2reuimp0 45247 ichexmpl1 45562 lcoss 46418 |
Copyright terms: Public domain | W3C validator |