![]() |
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 215 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
3 | 2 | necon3abid 3003 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
4 | 3 | bicomd 215 | 1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 = wceq 1507 ≠ wne 2967 |
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 199 df-ne 2968 |
This theorem is referenced by: necon1abid 3005 necon3bid 3011 eldifsn 4593 php 8497 xmullem2 12474 seqcoll2 13636 cnpart 14460 rlimrecl 14798 ncoprmgcdne1b 15850 prmrp 15912 4sqlem17 16153 mrieqvd 16767 mrieqv2d 16768 pltval 17428 latnlemlt 17552 latnle 17553 odnncl 18435 gexnnod 18474 sylow1lem1 18484 slwpss 18498 lssnle 18558 lspsnne1 19611 nzrunit 19761 psrridm 19898 cnsubrg 20307 cmpfi 21720 hausdiag 21957 txhaus 21959 isusp 22573 recld2 23125 metdseq0 23165 i1f1lem 23993 aaliou2b 24633 dvloglem 24932 logf1o2 24934 lgsne0 25613 lgsqr 25629 2sqlem7 25702 ostth3 25916 tglngne 26038 tgelrnln 26118 eucrct2eupthOLD 27776 eucrct2eupth 27777 norm1exi 28806 atnemeq0 29935 opeldifid 30115 qtophaus 30750 ordtconnlem1 30817 elzrhunit 30870 sgnneg 31450 subfacp1lem6 32023 maxidln1 34770 smprngopr 34778 lsatnem0 35632 atncmp 35899 atncvrN 35902 cdlema2N 36379 lhpmatb 36618 lhpat3 36633 cdleme3 36824 cdleme7 36836 cdlemg27b 37283 dvh2dimatN 38027 dvh2dim 38032 dochexmidlem1 38047 dochfln0 38064 |
Copyright terms: Public domain | W3C validator |