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 2936 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3abii.1 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑) | |
3 | 1, 2 | xchbinx 337 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 = wceq 1543 ≠ wne 2935 |
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 210 df-ne 2936 |
This theorem is referenced by: necon3bbii 2982 necon3bii 2987 nesym 2991 rabn0 4290 xpimasn 6037 rankxplim3 9480 rankxpsuc 9481 dflt2 12721 gcd0id 16059 lcmfunsnlem2 16178 axlowdimlem13 27017 hashxpe 30819 ssmxidllem 31327 fedgmullem2 31397 gonanegoal 32999 filnetlem4 34264 dihatlat 39042 pellex 40312 nev 41007 ldepspr 45441 |
Copyright terms: Public domain | W3C validator |