![]() |
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 3015 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
3 | df-ne 2970 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
4 | 2, 3 | bitr4i 270 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 = wceq 1601 ≠ wne 2969 |
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 199 df-ne 2970 |
This theorem is referenced by: necom 3022 neeq1i 3033 neeq2i 3034 neeq12i 3035 rnsnn0 5857 onoviun 7725 onnseq 7726 intrnfi 8612 wdomtr 8771 noinfep 8856 wemapwe 8893 scott0s 9050 cplem1 9051 karden 9057 acndom2 9212 dfac5lem3 9283 fin23lem31 9502 fin23lem40 9510 isf34lem5 9537 isf34lem7 9538 isf34lem6 9539 axrrecex 10322 negne0bi 10698 rpnnen1lem4 12132 rpnnen1lem5 12133 fseqsupcl 13100 limsupgre 14629 isercolllem3 14814 rpnnen2lem12 15367 ruclem11 15382 3dvds 15469 prmreclem6 16040 0ram 16139 0ram2 16140 0ramcl 16142 gsumval2 17677 ghmrn 18068 gexex 18653 gsumval3 18705 iinopn 21125 cnconn 21645 1stcfb 21668 qtopeu 21939 fbasrn 22107 alexsublem 22267 evth 23177 minveclem1 23641 minveclem3b 23645 ovollb2 23704 ovolunlem1a 23711 ovolunlem1 23712 ovoliunlem1 23717 ovoliun2 23721 ioombl1lem4 23776 uniioombllem1 23796 uniioombllem2 23798 uniioombllem6 23803 mbfsup 23879 mbfinf 23880 mbflimsup 23881 itg1climres 23929 itg2monolem1 23965 itg2mono 23968 itg2i1fseq2 23971 sincos4thpi 24714 axlowdimlem13 26320 eulerpath 27662 siii 28297 minvecolem1 28319 bcsiALT 28625 h1de2bi 29002 h1de2ctlem 29003 nmlnopgt0i 29445 dimval 30429 dimvalfi 30430 rge0scvg 30601 erdszelem5 31784 cvmsss2 31863 elrn3 32254 nosepnelem 32427 rankeq1o 32875 fin2so 34030 heicant 34079 scottn0f 34610 psspwb 38136 fnwe2lem2 38594 wnefimgd 39430 |
Copyright terms: Public domain | W3C validator |