![]() |
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 2943 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
4 | 1, 3 | pm2.21dd 195 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ≠ wne 2938 |
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 207 df-ne 2939 |
This theorem is referenced by: cshwshashlem2 17131 dprdsn 20071 ablsimpgfind 20145 coseq00topi 26559 tglndim0 28652 ncolncol 28669 footne 28746 s3f1 32916 chnub 32986 cycpmco2lem7 33135 fracfld 33290 linds2eq 33389 dfufd2lem 33557 ply1dg3rt0irred 33587 ig1pmindeg 33602 sgnsub 34526 sgnmulsgn 34531 sgnmulsgp 34532 pconnconn 35216 irrdifflemf 37308 osumcllem11N 39949 dochexmidlem8 41450 sticksstones22 42150 exp11d 42340 remul01 42414 fnchoice 44967 |
Copyright terms: Public domain | W3C validator |