![]() |
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 2944 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
4 | 1, 3 | pm2.21dd 194 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ≠ wne 2939 |
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 206 df-ne 2940 |
This theorem is referenced by: cshwshashlem2 17035 dprdsn 19948 ablsimpgfind 20022 coseq00topi 26245 tglndim0 28144 ncolncol 28161 footne 28238 s3f1 32377 cycpmco2lem7 32558 linds2eq 32768 ig1pmindeg 32944 sgnsub 33838 sgnmulsgn 33843 sgnmulsgp 33844 pconnconn 34517 irrdifflemf 36510 osumcllem11N 39141 dochexmidlem8 40642 sticksstones22 41291 exp11d 41519 remul01 41583 fnchoice 44016 |
Copyright terms: Public domain | W3C validator |