Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon3bbid | Structured version Visualization version GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.) |
Ref | Expression |
---|---|
necon3bbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) |
Ref | Expression |
---|---|
necon3bbid | ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3bbid.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) | |
2 | 1 | bicomd 224 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
3 | 2 | necon3abid 3049 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
4 | 3 | bicomd 224 | 1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 = wceq 1528 ≠ wne 3013 |
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 3014 |
This theorem is referenced by: necon1abid 3051 necon3bid 3057 eldifsn 4711 php 8689 xmullem2 12646 seqcoll2 13811 cnpart 14587 rlimrecl 14925 ncoprmgcdne1b 15982 prmrp 16044 4sqlem17 16285 mrieqvd 16897 mrieqv2d 16898 pltval 17558 latnlemlt 17682 latnle 17683 odnncl 18602 gexnnod 18642 sylow1lem1 18652 slwpss 18666 lssnle 18729 lspsnne1 19818 nzrunit 19968 psrridm 20112 cnsubrg 20533 cmpfi 21944 hausdiag 22181 txhaus 22183 isusp 22797 recld2 23349 metdseq0 23389 i1f1lem 24217 aaliou2b 24857 dvloglem 25158 logf1o2 25160 lgsne0 25838 lgsqr 25854 2sqlem7 25927 ostth3 26141 tglngne 26263 tgelrnln 26343 eucrct2eupth 27951 norm1exi 28954 atnemeq0 30081 opeldifid 30277 qtophaus 30999 ordtconnlem1 31066 elzrhunit 31119 sgnneg 31697 subfacp1lem6 32329 maxidln1 35203 smprngopr 35211 lsatnem0 36061 atncmp 36328 atncvrN 36331 cdlema2N 36808 lhpmatb 37047 lhpat3 37062 cdleme3 37253 cdleme7 37265 cdlemg27b 37712 dvh2dimatN 38456 dvh2dim 38461 dochexmidlem1 38476 dochfln0 38493 |
Copyright terms: Public domain | W3C validator |