Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > necon3bid | GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
necon3bid.1 | ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) |
Ref | Expression |
---|---|
necon3bid | ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2328 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3bid.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) | |
3 | 2 | necon3bbid 2367 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷)) |
4 | 1, 3 | syl5bb 191 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 104 = wceq 1335 ≠ wne 2327 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 |
This theorem depends on definitions: df-bi 116 df-ne 2328 |
This theorem is referenced by: nebidc 2407 addneintrd 8063 addneintr2d 8064 negne0bd 8179 negned 8183 subne0d 8195 subne0ad 8197 subneintrd 8230 subneintr2d 8232 qapne 9548 xrlttri3 9704 xaddass2 9774 sqne0 10484 fihashneq0 10669 hashnncl 10670 cjne0 10808 absne0d 11087 sqrt2irraplemnn 12054 metn0 12789 |
Copyright terms: Public domain | W3C validator |