|   | 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 2014 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | |
| 2 | equtr 2019 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧)) | |
| 3 | 1, 2 | impbid 212 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 | 
| This theorem is referenced by: equvinv 2027 equvelv 2029 spaev 2051 sbjust 2062 equsb3 2102 cbvsbvf 2365 drsb1 2499 mo4 2565 sb8eulem 2597 cbvmovw 2601 cbvmow 2602 axextg 2709 reu6 3731 reu7 3737 reu8nf 3876 disjxun 5140 solin 5618 cbviotaw 6520 cbviota 6522 dff13f 7277 poxp 8154 poxp2 8169 poxp3 8176 unxpdomlem1 9287 unxpdomlem2 9288 aceq0 10159 zfac 10501 axrepndlem1 10633 zfcndac 10660 injresinj 13828 fsum2dlem 15807 ramub1lem2 17066 ramcl 17068 symgextf1 19440 mamulid 22448 mamurid 22449 mdetdiagid 22607 mdetunilem9 22627 alexsubALTlem3 24058 ptcmplem2 24062 dscmet 24586 dyadmbllem 25635 opnmbllem 25637 isppw2 27159 2sqreulem1 27491 2sqreunnlem1 27494 frgr2wwlk1 30349 disji2f 32591 disjif2 32595 cbvmodavw 36252 cbvsbdavw 36256 cbvsbdavw2 36257 bj-ssblem1 36656 bj-ssblem2 36657 cbveud 37374 wl-naevhba1v 37522 wl-equsb3 37558 mblfinlem1 37665 bfp 37832 dveeq1-o 38937 dveeq1-o16 38938 axc11n-16 38940 ax12eq 38943 aks6d1c6lem3 42174 aks6d1c7 42186 fsuppind 42605 eu6w 42691 fphpd 42832 ax6e2nd 44583 ax6e2ndVD 44933 ax6e2ndALT 44955 disjinfi 45202 iundjiun 46480 hspdifhsp 46636 hspmbl 46649 2reu8i 47130 2reuimp0 47131 ichexmpl1 47461 lcoss 48358 | 
| Copyright terms: Public domain | W3C validator |