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 3052 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
4 | 3 | bicomd 224 | 1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ 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: necon1abid 3054 necon3bid 3060 eldifsn 4713 php 8690 xmullem2 12648 seqcoll2 13813 cnpart 14589 rlimrecl 14927 ncoprmgcdne1b 15984 prmrp 16046 4sqlem17 16287 mrieqvd 16899 mrieqv2d 16900 pltval 17560 latnlemlt 17684 latnle 17685 odnncl 18604 gexnnod 18644 sylow1lem1 18654 slwpss 18668 lssnle 18731 lspsnne1 19820 nzrunit 19970 psrridm 20114 cnsubrg 20535 cmpfi 21946 hausdiag 22183 txhaus 22185 isusp 22799 recld2 23351 metdseq0 23391 i1f1lem 24219 aaliou2b 24859 dvloglem 25158 logf1o2 25160 lgsne0 25839 lgsqr 25855 2sqlem7 25928 ostth3 26142 tglngne 26264 tgelrnln 26344 eucrct2eupth 27952 norm1exi 28955 atnemeq0 30082 opeldifid 30278 qtophaus 31000 ordtconnlem1 31067 elzrhunit 31120 sgnneg 31698 subfacp1lem6 32330 maxidln1 35205 smprngopr 35213 lsatnem0 36063 atncmp 36330 atncvrN 36333 cdlema2N 36810 lhpmatb 37049 lhpat3 37064 cdleme3 37255 cdleme7 37267 cdlemg27b 37714 dvh2dimatN 38458 dvh2dim 38463 dochexmidlem1 38478 dochfln0 38495 |
Copyright terms: Public domain | W3C validator |