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 2935 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | syl6ib 254 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵)) |
4 | 3 | con2d 136 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2934 |
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 2935 |
This theorem is referenced by: necon4bd 2954 necon4d 2958 minel 4355 disjiun 5017 eceqoveq 8433 en3lp 9150 infpssrlem5 9807 nneo 12147 zeo2 12150 sqrt2irr 15694 bezoutr1 16010 coprm 16152 dfphi2 16211 pltirr 17689 oddvdsnn0 18790 psgnodpmr 20406 supnfcls 22771 flimfnfcls 22779 metds0 23602 metdseq0 23606 metnrmlem1a 23610 sineq0 25268 lgsqr 26087 staddi 30181 stadd3i 30183 eulerpartlems 31897 erdszelem8 32731 finminlem 34150 ordcmp 34279 poimirlem18 35438 poimirlem21 35441 cvrnrefN 36939 trlnidatb 37834 flt4lem2 40076 |
Copyright terms: Public domain | W3C validator |