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 2828 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
3 | df-ne 2782 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
4 | 2, 3 | bitr4i 266 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 = wceq 1475 ≠ wne 2780 |
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 196 df-ne 2782 |
This theorem is referenced by: necom 2835 neeq1i 2846 neeq2i 2847 neeq12i 2848 rnsnn0 5519 onoviun 7327 onnseq 7328 intrnfi 8205 wdomtr 8363 noinfep 8440 wemapwe 8477 scott0s 8634 cplem1 8635 karden 8641 acndom2 8760 dfac5lem3 8831 fin23lem31 9048 fin23lem40 9056 isf34lem5 9083 isf34lem7 9084 isf34lem6 9085 axrrecex 9863 negne0bi 10233 rpnnen1lem4 11693 rpnnen1lem5 11694 rpnnen1lem4OLD 11699 rpnnen1lem5OLD 11700 fseqsupcl 12638 limsupgre 14060 isercolllem3 14245 rpnnen2lem12 14793 ruclem11 14808 3dvds 14890 3dvdsOLD 14891 prmreclem6 15463 0ram 15562 0ram2 15563 0ramcl 15565 gsumval2 17103 ghmrn 17496 gexex 18079 gsumval3 18131 iinopn 20532 cnconn 21035 1stcfb 21058 qtopeu 21329 fbasrn 21498 alexsublem 21658 evth 22566 minveclem1 23003 minveclem3b 23007 ovollb2 23064 ovolunlem1a 23071 ovolunlem1 23072 ovoliunlem1 23077 ovoliun2 23081 ioombl1lem4 23136 uniioombllem1 23155 uniioombllem2 23157 uniioombllem6 23162 mbfsup 23237 mbfinf 23238 mbflimsup 23239 itg1climres 23287 itg2monolem1 23323 itg2mono 23326 itg2i1fseq2 23329 sincos4thpi 24069 axlowdimlem13 25634 eupath 26508 siii 27092 minvecolem1 27114 bcsiALT 27420 h1de2bi 27797 h1de2ctlem 27798 nmlnopgt0i 28240 rge0scvg 29323 erdszelem5 30431 cvmsss2 30510 elrn3 30906 rankeq1o 31448 fin2so 32566 heicant 32614 scottn0f 33148 fnwe2lem2 36639 wnefimgd 37480 eulerpath 41409 |
Copyright terms: Public domain | W3C validator |