| 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 3006 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
| 3 | df-ne 2961 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
| 4 | 2, 3 | bitr4i 281 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 209 = wceq 1563 ≠ wne 2960 |
| 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 210 df-ne 2961 |
| This theorem is referenced by: necom 3013 neeq1i 3024 neeq2i 3025 neeq12i 3026 rnsnn0 6199 onoviun 8318 onnseq 8319 intrnfi 9364 wdomtr 9525 noinfep 9617 wemapwe 9654 scott0s 9850 cplem1 9863 karden 9869 acndom2 10026 dfac5lem3 10097 fin23lem31 10315 fin23lem40 10323 isf34lem5 10350 isf34lem7 10351 isf34lem6 10352 axrrecex 11136 negne0bi 11519 rpnnen1lem4 12995 rpnnen1lem5 12996 fseqsupcl 14004 limsupgre 15522 isercolllem3 15708 rpnnen2lem12 16271 ruclem11 16286 3dvds 16379 prmreclem6 16971 0ram 17070 0ram2 17071 0ramcl 17073 gsumval2 18734 ghmrn 19290 gexex 19914 gsumval3 19968 subdrgint 20875 iinopn 23020 cnconn 23540 1stcfb 23563 qtopeu 23834 fbasrn 24002 alexsublem 24162 evth 25079 minveclem1 25544 minveclem3b 25548 ovollb2 25609 ovolunlem1a 25616 ovolunlem1 25617 ovoliunlem1 25622 ovoliun2 25626 ioombl1lem4 25681 uniioombllem1 25701 uniioombllem2 25703 uniioombllem6 25708 mbfsup 25784 mbfinf 25785 mbflimsup 25786 itg1climres 25834 itg2monolem1 25870 itg2mono 25873 itg2i1fseq2 25876 sincos4thpi 26636 nosepnelem 27801 axlowdimlem13 29213 eulerpath 30501 siii 31114 minvecolem1 31135 bcsiALT 31440 h1de2bi 31815 h1de2ctlem 31816 nmlnopgt0i 32258 wrdpmtrlast 33326 dimval 33908 dimvalfi 33909 rge0scvg 34256 umgracycusgr 35517 cusgracyclt3v 35519 erdszelem5 35558 cvmsss2 35637 elrn3 36125 rankeq1o 36534 ttc0elw 36900 ttc0el 36908 regsfromunir1 36913 fin2so 38118 heicant 38166 scottn0f 38681 psspwb 42859 fnwe2lem2 43640 sqrtcval 44229 |
| Copyright terms: Public domain | W3C validator |