![]() |
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 222 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
3 | 2 | necon3abid 2979 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
4 | 3 | bicomd 222 | 1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1542 ≠ wne 2942 |
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 2943 |
This theorem is referenced by: necon1abid 2981 necon3bid 2987 eldifsn 4746 php 9113 phpOLD 9125 xmullem2 13139 seqcoll2 14318 cnpart 15085 rlimrecl 15422 ncoprmgcdne1b 16486 prmrp 16548 4sqlem17 16793 mrieqvd 17478 mrieqv2d 17479 pltval 18181 latnlemlt 18321 latnle 18322 odnncl 19286 gexnnod 19329 sylow1lem1 19339 slwpss 19353 lssnle 19415 lspsnne1 20531 nzrunit 20690 cnsubrg 20810 psrridm 21325 mhpmulcl 21491 cmpfi 22711 hausdiag 22948 txhaus 22950 isusp 23565 recld2 24129 metdseq0 24169 i1f1lem 25005 aaliou2b 25653 dvloglem 25955 logf1o2 25957 lgsne0 26635 lgsqr 26651 2sqlem7 26724 ostth3 26938 tglngne 27321 tgelrnln 27401 eucrct2eupth 29018 norm1exi 30021 atnemeq0 31148 opeldifid 31345 pridln1 32035 mxidln1 32055 ssmxidllem 32058 qtophaus 32221 ordtconnlem1 32309 elzrhunit 32364 sgnneg 32944 subfacp1lem6 33583 maxidln1 36435 smprngopr 36443 lsatnem0 37439 atncmp 37706 atncvrN 37709 cdlema2N 38187 lhpmatb 38426 lhpat3 38441 cdleme3 38632 cdleme7 38644 cdlemg27b 39091 dvh2dimatN 39835 dvh2dim 39840 dochexmidlem1 39855 dochfln0 39872 dvrelog2b 40455 aks6d1c2p2 40481 nna4b4nsq 40901 |
Copyright terms: Public domain | W3C validator |