![]() |
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 2811 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
4 | 3 | necon3bii 3021 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1653 ≠ wne 2969 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-ex 1876 df-cleq 2790 df-ne 2970 |
This theorem is referenced by: 3netr3g 3047 3netr4g 3048 oppchomfval 16684 oppcbas 16688 rescbas 16799 rescco 16802 rescabs 16803 odubas 17444 oppglem 18088 mgplem 18806 mgpress 18812 opprlem 18940 sralem 19496 srasca 19500 sravsca 19501 opsrbaslem 19796 zlmsca 20187 znbaslem 20204 thlbas 20361 thlle 20362 matsca 20542 tuslem 22395 setsmsbas 22604 setsmsds 22605 tngds 22776 ttgval 26103 ttglem 26104 cchhllem 26115 axlowdimlem6 26175 zlmds 30515 zlmtset 30516 nosepne 32335 hlhilslem 37950 zlmodzxzldeplem 43073 |
Copyright terms: Public domain | W3C validator |