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 3062 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷) |
3 | df-ne 3017 | . 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
4 | 2, 3 | bitr4i 279 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necom 3069 neeq1i 3080 neeq2i 3081 neeq12i 3082 rnsnn0 6059 onoviun 7971 onnseq 7972 intrnfi 8869 wdomtr 9028 noinfep 9112 wemapwe 9149 scott0s 9306 cplem1 9307 karden 9313 acndom2 9469 dfac5lem3 9540 fin23lem31 9754 fin23lem40 9762 isf34lem5 9789 isf34lem7 9790 isf34lem6 9791 axrrecex 10574 negne0bi 10948 rpnnen1lem4 12369 rpnnen1lem5 12370 fseqsupcl 13335 limsupgre 14828 isercolllem3 15013 rpnnen2lem12 15568 ruclem11 15583 3dvds 15670 prmreclem6 16247 0ram 16346 0ram2 16347 0ramcl 16349 gsumval2 17886 ghmrn 18311 gexex 18904 gsumval3 18958 subdrgint 19513 iinopn 21440 cnconn 21960 1stcfb 21983 qtopeu 22254 fbasrn 22422 alexsublem 22582 evth 23492 minveclem1 23956 minveclem3b 23960 ovollb2 24019 ovolunlem1a 24026 ovolunlem1 24027 ovoliunlem1 24032 ovoliun2 24036 ioombl1lem4 24091 uniioombllem1 24111 uniioombllem2 24113 uniioombllem6 24118 mbfsup 24194 mbfinf 24195 mbflimsup 24196 itg1climres 24244 itg2monolem1 24280 itg2mono 24283 itg2i1fseq2 24286 sincos4thpi 25028 axlowdimlem13 26668 eulerpath 27948 siii 28558 minvecolem1 28579 bcsiALT 28884 h1de2bi 29259 h1de2ctlem 29260 nmlnopgt0i 29702 dimval 30901 dimvalfi 30902 rge0scvg 31092 umgracycusgr 32299 cusgracyclt3v 32301 erdszelem5 32340 cvmsss2 32419 elrn3 32896 nosepnelem 33082 rankeq1o 33530 fin2so 34761 heicant 34809 scottn0f 35331 psspwb 38994 fnwe2lem2 39531 |
Copyright terms: Public domain | W3C validator |