![]() |
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 2988 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
3 | df-ne 2942 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
4 | 2, 3 | bitr4i 278 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1542 ≠ wne 2941 |
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 2942 |
This theorem is referenced by: necom 2995 neeq1i 3006 neeq2i 3007 neeq12i 3008 rnsnn0 6204 onoviun 8338 onnseq 8339 intrnfi 9407 wdomtr 9566 noinfep 9651 wemapwe 9688 scott0s 9879 cplem1 9880 karden 9886 acndom2 10045 dfac5lem3 10116 fin23lem31 10334 fin23lem40 10342 isf34lem5 10369 isf34lem7 10370 isf34lem6 10371 axrrecex 11154 negne0bi 11529 rpnnen1lem4 12960 rpnnen1lem5 12961 fseqsupcl 13938 limsupgre 15421 isercolllem3 15609 rpnnen2lem12 16164 ruclem11 16179 3dvds 16270 prmreclem6 16850 0ram 16949 0ram2 16950 0ramcl 16952 gsumval2 18601 ghmrn 19099 gexex 19713 gsumval3 19767 subdrgint 20407 iinopn 22386 cnconn 22908 1stcfb 22931 qtopeu 23202 fbasrn 23370 alexsublem 23530 evth 24457 minveclem1 24923 minveclem3b 24927 ovollb2 24988 ovolunlem1a 24995 ovolunlem1 24996 ovoliunlem1 25001 ovoliun2 25005 ioombl1lem4 25060 uniioombllem1 25080 uniioombllem2 25082 uniioombllem6 25087 mbfsup 25163 mbfinf 25164 mbflimsup 25165 itg1climres 25214 itg2monolem1 25250 itg2mono 25253 itg2i1fseq2 25256 sincos4thpi 26005 nosepnelem 27162 axlowdimlem13 28192 eulerpath 29474 siii 30084 minvecolem1 30105 bcsiALT 30410 h1de2bi 30785 h1de2ctlem 30786 nmlnopgt0i 31228 dimval 32632 dimvalfi 32633 rge0scvg 32867 umgracycusgr 34083 cusgracyclt3v 34085 erdszelem5 34124 cvmsss2 34203 elrn3 34670 rankeq1o 35081 fin2so 36413 heicant 36461 scottn0f 36976 psspwb 40994 fnwe2lem2 41726 sqrtcval 42325 |
Copyright terms: Public domain | W3C validator |