![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3abii | Structured version Visualization version GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.) |
Ref | Expression |
---|---|
necon3abii.1 | ⊢ (𝐴 = 𝐵 ↔ 𝜑) |
Ref | Expression |
---|---|
necon3abii | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 3000 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3abii.1 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑) | |
3 | 1, 2 | xchbinx 326 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 = wceq 1656 ≠ wne 2999 |
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 199 df-ne 3000 |
This theorem is referenced by: necon3bbii 3046 necon3bii 3051 nesym 3055 rabn0 4187 xpimasn 5820 rankxplim3 9021 rankxpsuc 9022 dflt2 12267 gcd0id 15613 lcmfunsnlem2 15726 axlowdimlem13 26253 filnetlem4 32903 dihatlat 37402 pellex 38236 nev 38896 ldepspr 43102 |
Copyright terms: Public domain | W3C validator |