Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neeq12i | Structured version Visualization version GIF version |
Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Ref | Expression |
---|---|
neeq1i.1 | ⊢ 𝐴 = 𝐵 |
neeq12i.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
neeq12i | ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | neeq12i.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
3 | 1, 2 | eqeq12i 2754 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
4 | 3 | necon3bii 2987 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1542 ≠ wne 2935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-cleq 2731 df-ne 2936 |
This theorem is referenced by: 3netr3g 3013 3netr4g 3014 oppchomfval 17101 oppcbas 17105 rescbas 17217 rescco 17220 rescabs 17221 odubas 17872 oppglem 18609 mgplem 19376 mgpress 19382 opprlem 19513 sralem 20081 srasca 20085 sravsca 20086 zlmsca 20354 znbaslem 20370 thlbas 20525 thlle 20526 opsrbaslem 20873 matsca 21179 tuslem 23032 setsmsbas 23241 setsmsds 23242 tngds 23414 ttgval 26834 ttglem 26835 cchhllem 26846 axlowdimlem6 26906 zlmds 31497 zlmtset 31498 nosepne 33539 hlhilslem 39608 zlmodzxzldeplem 45421 line2 45680 prstcleval 45856 prstcocval 45858 |
Copyright terms: Public domain | W3C validator |