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 3017 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3abii.1 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑) | |
3 | 1, 2 | xchbinx 335 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necon3bbii 3063 necon3bii 3068 nesym 3072 rabn0 4338 xpimasn 6036 rankxplim3 9299 rankxpsuc 9300 dflt2 12531 gcd0id 15857 lcmfunsnlem2 15974 axlowdimlem13 26668 hashxpe 30456 fedgmullem2 30926 gonanegoal 32497 filnetlem4 33627 dihatlat 38352 pellex 39312 nev 39995 ldepspr 44426 |
Copyright terms: Public domain | W3C validator |