Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon3bii | Structured version Visualization version GIF version |
Description: Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.) |
Ref | Expression |
---|---|
necon3bii.1 | ⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) |
Ref | Expression |
---|---|
necon3bii | ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3bii.1 | . . 3 ⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) | |
2 | 1 | necon3abii 2840 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
3 | df-ne 2795 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
4 | 2, 3 | bitr4i 267 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 = wceq 1483 ≠ wne 2794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-ne 2795 |
This theorem is referenced by: necom 2847 neeq1i 2858 neeq2i 2859 neeq12i 2860 rnsnn0 5601 onoviun 7440 onnseq 7441 intrnfi 8322 wdomtr 8480 noinfep 8557 wemapwe 8594 scott0s 8751 cplem1 8752 karden 8758 acndom2 8877 dfac5lem3 8948 fin23lem31 9165 fin23lem40 9173 isf34lem5 9200 isf34lem7 9201 isf34lem6 9202 axrrecex 9984 negne0bi 10354 rpnnen1lem4 11817 rpnnen1lem5 11818 rpnnen1lem4OLD 11823 rpnnen1lem5OLD 11824 fseqsupcl 12776 limsupgre 14212 isercolllem3 14397 rpnnen2lem12 14954 ruclem11 14969 3dvds 15052 3dvdsOLD 15053 prmreclem6 15625 0ram 15724 0ram2 15725 0ramcl 15727 gsumval2 17280 ghmrn 17673 gexex 18256 gsumval3 18308 iinopn 20707 cnconn 21225 1stcfb 21248 qtopeu 21519 fbasrn 21688 alexsublem 21848 evth 22758 minveclem1 23195 minveclem3b 23199 ovollb2 23257 ovolunlem1a 23264 ovolunlem1 23265 ovoliunlem1 23270 ovoliun2 23274 ioombl1lem4 23329 uniioombllem1 23349 uniioombllem2 23351 uniioombllem6 23356 mbfsup 23431 mbfinf 23432 mbflimsup 23433 itg1climres 23481 itg2monolem1 23517 itg2mono 23520 itg2i1fseq2 23523 sincos4thpi 24265 axlowdimlem13 25834 eulerpath 27101 siii 27708 minvecolem1 27730 bcsiALT 28036 h1de2bi 28413 h1de2ctlem 28414 nmlnopgt0i 28856 rge0scvg 29995 erdszelem5 31177 cvmsss2 31256 elrn3 31652 nosepnelem 31830 rankeq1o 32278 fin2so 33396 heicant 33444 scottn0f 33978 fnwe2lem2 37621 wnefimgd 38460 |
Copyright terms: Public domain | W3C validator |