Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neeq12d | Structured version Visualization version GIF version |
Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Ref | Expression |
---|---|
neeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
neeq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
neeq12d | ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | neeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
3 | 1, 2 | eqeq12d 2837 | . 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
4 | 3 | necon3bid 3060 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ 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: 2nreu 4391 fnelnfp 6932 suppval 7823 infpssrlem4 9717 injresinjlem 13147 sgrp2nmndlem5 18034 pmtr3ncom 18534 isnzr 19962 ptcmplem2 22591 isinag 26552 axlowdimlem6 26661 axlowdimlem14 26669 pthdadjvtx 27439 uhgrwkspthlem2 27463 usgr2wlkspth 27468 usgr2trlncl 27469 pthdlem1 27475 lfgrn1cycl 27511 2wlkdlem5 27636 2pthdlem1 27637 3wlkdlem5 27870 3pthdlem1 27871 numclwwlkovh0 28079 numclwwlk2lem1 28083 numclwlk2lem2f 28084 numclwlk2lem2f1o 28086 eulplig 28190 signsvvfval 31748 signsvfn 31752 bnj1534 32025 bnj1542 32029 bnj1280 32190 derangsn 32315 derangenlem 32316 subfacp1lem3 32327 subfacp1lem5 32329 subfacp1lem6 32330 subfacp1 32331 sltval2 33061 sltres 33067 noseponlem 33069 noextenddif 33073 nosepnelem 33082 nosepeq 33087 nosupbnd2lem1 33113 noetalem3 33117 fvtransport 33391 poimirlem1 34775 poimirlem6 34780 poimirlem7 34781 cdlemkid3N 37951 cdlemkid4 37952 stoweidlem43 42209 ichnreuop 43481 nnsgrpnmnd 43932 2zrngnmlid 44118 pgrpgt2nabl 44312 ldepsnlinc 44461 |
Copyright terms: Public domain | W3C validator |