Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2.21ddne | Structured version Visualization version GIF version |
Description: A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) |
Ref | Expression |
---|---|
pm2.21ddne.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
pm2.21ddne.2 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
Ref | Expression |
---|---|
pm2.21ddne | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21ddne.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | pm2.21ddne.2 | . . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
3 | 2 | neneqd 3021 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
4 | 1, 3 | pm2.21dd 196 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: cshwshashlem2 16420 dprdsn 19089 ablsimpgfind 19163 coseq00topi 25017 tglndim0 26343 ncolncol 26360 footne 26437 s3f1 30551 cycpmco2lem7 30702 linds2eq 30869 sgnsub 31702 sgnmulsgn 31707 sgnmulsgp 31708 pconnconn 32376 osumcllem11N 36984 dochexmidlem8 38485 remul01 39117 fnchoice 41166 |
Copyright terms: Public domain | W3C validator |