| 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 2987 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
| 3 | df-ne 2941 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
| 4 | 2, 3 | bitr4i 278 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 = wceq 1540 ≠ wne 2940 |
| 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 207 df-ne 2941 |
| This theorem is referenced by: necom 2994 neeq1i 3005 neeq2i 3006 neeq12i 3007 rnsnn0 6228 onoviun 8383 onnseq 8384 intrnfi 9456 wdomtr 9615 noinfep 9700 wemapwe 9737 scott0s 9928 cplem1 9929 karden 9935 acndom2 10094 dfac5lem3 10165 fin23lem31 10383 fin23lem40 10391 isf34lem5 10418 isf34lem7 10419 isf34lem6 10420 axrrecex 11203 negne0bi 11582 rpnnen1lem4 13022 rpnnen1lem5 13023 fseqsupcl 14018 limsupgre 15517 isercolllem3 15703 rpnnen2lem12 16261 ruclem11 16276 3dvds 16368 prmreclem6 16959 0ram 17058 0ram2 17059 0ramcl 17061 gsumval2 18699 ghmrn 19247 gexex 19871 gsumval3 19925 subdrgint 20804 iinopn 22908 cnconn 23430 1stcfb 23453 qtopeu 23724 fbasrn 23892 alexsublem 24052 evth 24991 minveclem1 25458 minveclem3b 25462 ovollb2 25524 ovolunlem1a 25531 ovolunlem1 25532 ovoliunlem1 25537 ovoliun2 25541 ioombl1lem4 25596 uniioombllem1 25616 uniioombllem2 25618 uniioombllem6 25623 mbfsup 25699 mbfinf 25700 mbflimsup 25701 itg1climres 25749 itg2monolem1 25785 itg2mono 25788 itg2i1fseq2 25791 sincos4thpi 26555 nosepnelem 27724 axlowdimlem13 28969 eulerpath 30260 siii 30872 minvecolem1 30893 bcsiALT 31198 h1de2bi 31573 h1de2ctlem 31574 nmlnopgt0i 32016 wrdpmtrlast 33113 dimval 33651 dimvalfi 33652 rge0scvg 33948 umgracycusgr 35159 cusgracyclt3v 35161 erdszelem5 35200 cvmsss2 35279 elrn3 35762 rankeq1o 36172 fin2so 37614 heicant 37662 scottn0f 38177 psspwb 42267 fnwe2lem2 43063 sqrtcval 43654 |
| Copyright terms: Public domain | W3C validator |