![]() |
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 2977 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
3 | df-ne 2931 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
4 | 2, 3 | bitr4i 277 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1534 ≠ wne 2930 |
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 206 df-ne 2931 |
This theorem is referenced by: necom 2984 neeq1i 2995 neeq2i 2996 neeq12i 2997 rnsnn0 6209 onoviun 8362 onnseq 8363 intrnfi 9449 wdomtr 9608 noinfep 9693 wemapwe 9730 scott0s 9921 cplem1 9922 karden 9928 acndom2 10087 dfac5lem3 10158 fin23lem31 10374 fin23lem40 10382 isf34lem5 10409 isf34lem7 10410 isf34lem6 10411 axrrecex 11194 negne0bi 11571 rpnnen1lem4 13007 rpnnen1lem5 13008 fseqsupcl 13988 limsupgre 15475 isercolllem3 15663 rpnnen2lem12 16219 ruclem11 16234 3dvds 16325 prmreclem6 16915 0ram 17014 0ram2 17015 0ramcl 17017 gsumval2 18671 ghmrn 19216 gexex 19844 gsumval3 19898 subdrgint 20775 iinopn 22889 cnconn 23411 1stcfb 23434 qtopeu 23705 fbasrn 23873 alexsublem 24033 evth 24970 minveclem1 25437 minveclem3b 25441 ovollb2 25503 ovolunlem1a 25510 ovolunlem1 25511 ovoliunlem1 25516 ovoliun2 25520 ioombl1lem4 25575 uniioombllem1 25595 uniioombllem2 25597 uniioombllem6 25602 mbfsup 25678 mbfinf 25679 mbflimsup 25680 itg1climres 25729 itg2monolem1 25765 itg2mono 25768 itg2i1fseq2 25771 sincos4thpi 26535 nosepnelem 27703 axlowdimlem13 28882 eulerpath 30168 siii 30780 minvecolem1 30801 bcsiALT 31106 h1de2bi 31481 h1de2ctlem 31482 nmlnopgt0i 31924 wrdpmtrlast 32972 dimval 33498 dimvalfi 33499 rge0scvg 33774 umgracycusgr 34992 cusgracyclt3v 34994 erdszelem5 35033 cvmsss2 35112 elrn3 35594 rankeq1o 36005 fin2so 37318 heicant 37366 scottn0f 37881 psspwb 41969 fnwe2lem2 42746 sqrtcval 43342 |
Copyright terms: Public domain | W3C validator |