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 226 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
3 | 2 | necon3abid 2971 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
4 | 3 | bicomd 226 | 1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 = wceq 1543 ≠ wne 2935 |
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 210 df-ne 2936 |
This theorem is referenced by: necon1abid 2973 necon3bid 2979 eldifsn 4690 php 8819 xmullem2 12838 seqcoll2 14014 cnpart 14786 rlimrecl 15124 ncoprmgcdne1b 16188 prmrp 16250 4sqlem17 16495 mrieqvd 17113 mrieqv2d 17114 pltval 17810 latnlemlt 17950 latnle 17951 odnncl 18909 gexnnod 18949 sylow1lem1 18959 slwpss 18973 lssnle 19036 lspsnne1 20126 nzrunit 20277 cnsubrg 20395 psrridm 20901 mhpmulcl 21061 cmpfi 22277 hausdiag 22514 txhaus 22516 isusp 23131 recld2 23683 metdseq0 23723 i1f1lem 24558 aaliou2b 25206 dvloglem 25508 logf1o2 25510 lgsne0 26188 lgsqr 26204 2sqlem7 26277 ostth3 26491 tglngne 26613 tgelrnln 26693 eucrct2eupth 28300 norm1exi 29303 atnemeq0 30430 opeldifid 30629 pridln1 31304 mxidln1 31324 ssmxidllem 31327 qtophaus 31472 ordtconnlem1 31560 elzrhunit 31613 sgnneg 32191 subfacp1lem6 32832 maxidln1 35896 smprngopr 35904 lsatnem0 36753 atncmp 37020 atncvrN 37023 cdlema2N 37500 lhpmatb 37739 lhpat3 37754 cdleme3 37945 cdleme7 37957 cdlemg27b 38404 dvh2dimatN 39148 dvh2dim 39153 dochexmidlem1 39168 dochfln0 39185 dvrelog2b 39764 nna4b4nsq 40152 |
Copyright terms: Public domain | W3C validator |