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 1930 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | |
2 | equtr 1935 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧)) | |
3 | 1, 2 | impbid 201 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: equequ2OLD 1942 spaev 1965 drsb1 2365 equsb3lem 2419 sb8eu 2491 axext3ALT 2593 reu6 3362 reu7 3368 disjxun 4581 cbviota 5773 dff13f 6417 poxp 7176 unxpdomlem1 8049 unxpdomlem2 8050 aceq0 8824 zfac 9165 axrepndlem1 9293 zfcndac 9320 injresinj 12451 fsum2dlem 14343 ramub1lem2 15569 ramcl 15571 symgextf1 17664 mamulid 20066 mamurid 20067 mdetdiagid 20225 mdetunilem9 20245 alexsubALTlem3 21663 ptcmplem2 21667 dscmet 22187 dyadmbllem 23173 opnmbllem 23175 isppw2 24641 frg2wot1 26584 disji2f 28772 disjif2 28776 bj-ssblem1 31819 bj-ssblem2 31820 bj-axext3 31957 wl-naevhba1v 32483 wl-equsb3 32516 mblfinlem1 32616 bfp 32793 dveeq1-o 33238 dveeq1-o16 33239 axc11n-16 33241 ax12eq 33244 fphpd 36398 ax6e2nd 37795 ax6e2ndVD 38166 ax6e2ndALT 38188 disjinfi 38375 iundjiun 39353 hspdifhsp 39506 hspmbl 39519 frgr2wwlk1 41494 lcoss 42019 |
Copyright terms: Public domain | W3C validator |