![]() |
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 213 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
3 | 2 | necon3abid 2859 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
4 | 3 | bicomd 213 | 1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 = wceq 1523 ≠ wne 2823 |
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 197 df-ne 2824 |
This theorem is referenced by: necon1abid 2861 necon3bid 2867 eldifsn 4350 php 8185 xmullem2 12133 seqcoll2 13287 cnpart 14024 rlimrecl 14355 ncoprmgcdne1b 15410 prmrp 15471 4sqlem17 15712 mrieqvd 16345 mrieqv2d 16346 pltval 17007 latnlemlt 17131 latnle 17132 odnncl 18010 gexnnod 18049 sylow1lem1 18059 slwpss 18073 lssnle 18133 lspsnne1 19165 nzrunit 19315 psrridm 19452 cnsubrg 19854 cmpfi 21259 hausdiag 21496 txhaus 21498 isusp 22112 recld2 22664 metdseq0 22704 i1f1lem 23501 aaliou2b 24141 dvloglem 24439 logf1o2 24441 lgsne0 25105 lgsqr 25121 2sqlem7 25194 ostth3 25372 tglngne 25490 tgelrnln 25570 eucrct2eupth 27223 norm1exi 28235 atnemeq0 29364 opeldifid 29538 qtophaus 30031 ordtconnlem1 30098 elzrhunit 30151 sgnneg 30730 subfacp1lem6 31293 maxidln1 33973 smprngopr 33981 lsatnem0 34650 atncmp 34917 atncvrN 34920 cdlema2N 35396 lhpmatb 35635 lhpat3 35650 cdleme3 35842 cdleme7 35854 cdlemg27b 36301 dvh2dimatN 37046 dvh2dim 37051 dochexmidlem1 37066 dochfln0 37083 |
Copyright terms: Public domain | W3C validator |