| 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 2039 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | |
| 2 | equtr 2044 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧)) | |
| 3 | 1, 2 | impbid 215 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1803 |
| This theorem is referenced by: equvinv 2052 equvelv 2054 spaev 2077 rename-sb 2092 equsb3 2140 cbvsbvf 2397 drsb1 2529 mo4 2596 sb8eulem 2628 cbvmovw 2632 cbvmow 2633 axextg 2739 reu6 3692 reu7 3698 reu8nf 3833 disjxun 5103 solin 5587 cbviotaw 6488 cbviota 6490 dff13f 7243 poxp 8112 poxp2 8127 poxp3 8134 unxpdomlem1 9204 unxpdomlem2 9205 aceq0 10090 zfac 10432 axrepndlem1 10565 zfcndac 10592 injresinj 13811 fsum2dlem 15811 ramub1lem2 17077 ramcl 17079 symgextf1 19482 mamulid 22559 mamurid 22560 mdetdiagid 22718 mdetunilem9 22738 alexsubALTlem3 24167 ptcmplem2 24171 dscmet 24690 dyadmbllem 25719 opnmbllem 25721 isppw2 27237 2sqreulem1 27568 2sqreunnlem1 27571 frgr2wwlk1 30589 disji2f 32832 disjif2 32836 cbvmodavw 36623 cbvsbdavw 36627 cbvsbdavw2 36628 axtcond 36851 dfttc4 36903 bj-ssblem1 37138 bj-ssblem2 37139 cbveud 37878 wl-naevhba1v 38035 wl-equsb3 38071 mblfinlem1 38168 bfp 38335 dveeq1-o 39571 dveeq1-o16 39572 axc11n-16 39574 ax12eq 39577 aks6d1c6lem3 42801 aks6d1c7 42813 fsuppind 43184 eu6w 43270 fphpd 43405 ax6e2nd 45132 ax6e2ndVD 45481 ax6e2ndALT 45503 disjinfi 45768 iundjiun 47032 hspdifhsp 47188 hspmbl 47201 2reu8i 47705 2reuimp0 47706 ichexmpl1 48073 lcoss 49067 |
| Copyright terms: Public domain | W3C validator |