![]() |
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 2969 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3abii.1 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑) | |
3 | 1, 2 | xchbinx 326 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 = wceq 1601 ≠ wne 2968 |
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 2969 |
This theorem is referenced by: necon3bbii 3015 necon3bii 3020 nesym 3024 rabn0 4187 xpimasn 5833 rankxplim3 9041 rankxpsuc 9042 dflt2 12291 gcd0id 15646 lcmfunsnlem2 15759 axlowdimlem13 26303 filnetlem4 32978 dihatlat 37482 pellex 38351 nev 39011 ldepspr 43269 |
Copyright terms: Public domain | W3C validator |