![]() |
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 2930 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3abii.1 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑) | |
3 | 1, 2 | xchbinx 333 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1533 ≠ wne 2929 |
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 2930 |
This theorem is referenced by: necon3bbii 2977 necon3bii 2982 nesym 2986 rabn0 4387 dffr6 5636 xpimasn 6191 rankxplim3 9906 rankxpsuc 9907 dflt2 13162 gcd0id 16497 lcmfunsnlem2 16614 axlowdimlem13 28837 hashxpe 32659 ssdifidllem 33268 ssmxidllem 33285 fedgmullem2 33456 gonanegoal 35090 filnetlem4 35993 dihatlat 40934 sn-00id 42088 pellex 42394 nev 43339 ldepspr 47724 |
Copyright terms: Public domain | W3C validator |