Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon2bd | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.) |
Ref | Expression |
---|---|
necon2bd.1 | ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Ref | Expression |
---|---|
necon2bd | ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2bd.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) | |
2 | df-ne 3017 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | syl6ib 252 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵)) |
4 | 3 | con2d 136 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necon4bd 3036 necon4d 3040 minel 4413 disjiun 5045 eceqoveq 8392 en3lp 9066 infpssrlem5 9718 nneo 12055 zeo2 12058 sqrt2irr 15592 bezoutr1 15903 coprm 16045 dfphi2 16101 pltirr 17563 oddvdsnn0 18603 psgnodpmr 20664 supnfcls 22558 flimfnfcls 22566 metds0 23387 metdseq0 23391 metnrmlem1a 23395 sineq0 25038 lgsqr 25855 staddi 29951 stadd3i 29953 eulerpartlems 31518 erdszelem8 32343 finminlem 33564 ordcmp 33693 poimirlem18 34792 poimirlem21 34795 cvrnrefN 36300 trlnidatb 37195 |
Copyright terms: Public domain | W3C validator |