![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3abid | Structured version Visualization version GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.) |
Ref | Expression |
---|---|
necon3abid.1 | ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
Ref | Expression |
---|---|
necon3abid | ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2824 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3abid.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) | |
3 | 2 | notbid 307 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓)) |
4 | 1, 3 | syl5bb 272 | 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: necon3bbid 2860 necon2abid 2865 foconst 6164 fndmdif 6361 suppsnop 7354 om00el 7701 oeoa 7722 cardsdom2 8852 mulne0b 10706 crne0 11051 expneg 12908 hashsdom 13208 prprrab 13293 gcdn0gt0 15286 cncongr2 15429 pltval3 17014 mulgnegnn 17598 drngmulne0 18817 lvecvsn0 19157 domnmuln0 19346 mvrf1 19473 connsub 21272 pthaus 21489 xkohaus 21504 bndth 22804 lebnumlem1 22807 dvcobr 23754 dvcnvlem 23784 mdegle0 23882 coemulhi 24055 vieta1lem1 24110 vieta1lem2 24111 aalioulem2 24133 cosne0 24321 atandm3 24650 wilthlem2 24840 issqf 24907 mumullem2 24951 dchrptlem3 25036 lgseisenlem3 25147 brbtwn2 25830 colinearalg 25835 vdn0conngrumgrv2 27174 vdgn1frgrv2 27276 nmlno0lem 27776 nmlnop0iALT 28982 atcvat2i 29374 divnumden2 29692 bnj1542 31053 bnj1253 31211 ptrecube 33539 poimirlem13 33552 ecinn0 34258 llnexchb2 35473 cdlemb3 36211 rencldnfilem 37701 qirropth 37790 binomcxplemfrat 38867 binomcxplemradcnv 38868 odz2prm2pw 41800 |
Copyright terms: Public domain | W3C validator |