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 2944 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | syl6ib 250 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵)) |
4 | 3 | con2d 134 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2943 |
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 2944 |
This theorem is referenced by: necon4bd 2963 necon4d 2967 minel 4399 disjiun 5061 eceqoveq 8611 en3lp 9372 infpssrlem5 10063 nneo 12404 zeo2 12407 sqrt2irr 15958 bezoutr1 16274 coprm 16416 dfphi2 16475 pltirr 18053 oddvdsnn0 19152 psgnodpmr 20795 supnfcls 23171 flimfnfcls 23179 metds0 24013 metdseq0 24017 metnrmlem1a 24021 sineq0 25680 lgsqr 26499 staddi 30608 stadd3i 30610 eulerpartlems 32327 erdszelem8 33160 finminlem 34507 ordcmp 34636 poimirlem18 35795 poimirlem21 35798 cvrnrefN 37296 trlnidatb 38191 flt4lem2 40484 |
Copyright terms: Public domain | W3C validator |