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 2836 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
4 | 3 | necon3bii 3068 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: 3netr3g 3094 3netr4g 3095 oppchomfval 16974 oppcbas 16978 rescbas 17089 rescco 17092 rescabs 17093 odubas 17733 oppglem 18418 mgplem 19175 mgpress 19181 opprlem 19309 sralem 19880 srasca 19884 sravsca 19885 opsrbaslem 20188 zlmsca 20598 znbaslem 20615 thlbas 20770 thlle 20771 matsca 20954 tuslem 22805 setsmsbas 23014 setsmsds 23015 tngds 23186 ttgval 26589 ttglem 26590 cchhllem 26601 axlowdimlem6 26661 zlmds 31105 zlmtset 31106 nosepne 33083 hlhilslem 38956 zlmodzxzldeplem 44451 line2 44637 |
Copyright terms: Public domain | W3C validator |