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 2946 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
4 | 1, 3 | pm2.21dd 198 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ≠ wne 2941 |
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 2942 |
This theorem is referenced by: cshwshashlem2 16674 dprdsn 19447 ablsimpgfind 19521 coseq00topi 25416 tglndim0 26744 ncolncol 26761 footne 26838 s3f1 30965 cycpmco2lem7 31142 linds2eq 31313 sgnsub 32247 sgnmulsgn 32252 sgnmulsgp 32253 pconnconn 32929 irrdifflemf 35256 osumcllem11N 37743 dochexmidlem8 39244 sticksstones22 39875 exp11d 40061 remul01 40126 fnchoice 42273 |
Copyright terms: Public domain | W3C validator |