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 2945 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
4 | 1, 3 | pm2.21dd 194 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ≠ wne 2940 |
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 2941 |
This theorem is referenced by: cshwshashlem2 16895 dprdsn 19734 ablsimpgfind 19808 coseq00topi 25765 tglndim0 27279 ncolncol 27296 footne 27373 s3f1 31508 cycpmco2lem7 31686 linds2eq 31872 sgnsub 32811 sgnmulsgn 32816 sgnmulsgp 32817 pconnconn 33492 irrdifflemf 35609 osumcllem11N 38242 dochexmidlem8 39743 sticksstones22 40389 exp11d 40593 remul01 40658 fnchoice 42901 |
Copyright terms: Public domain | W3C validator |