|   | 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 195 | 1 ⊢ (𝜑 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 ≠ 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 207 df-ne 2940 | 
| This theorem is referenced by: cshwshashlem2 17135 dprdsn 20057 ablsimpgfind 20131 coseq00topi 26545 tglndim0 28638 ncolncol 28655 footne 28732 s3f1 32932 chnub 33003 cycpmco2lem7 33153 fracfld 33311 linds2eq 33410 dfufd2lem 33578 ply1dg3rt0irred 33608 ig1pmindeg 33623 sgnsub 34548 sgnmulsgn 34553 sgnmulsgp 34554 pconnconn 35237 irrdifflemf 37327 osumcllem11N 39969 dochexmidlem8 41470 sticksstones22 42170 exp11d 42366 remul01 42442 fnchoice 45039 | 
| Copyright terms: Public domain | W3C validator |