![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61da2ne | Structured version Visualization version GIF version |
Description: Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.) |
Ref | Expression |
---|---|
pm2.61da2ne.1 | ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) |
pm2.61da2ne.2 | ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) |
pm2.61da2ne.3 | ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) |
Ref | Expression |
---|---|
pm2.61da2ne | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61da2ne.1 | . 2 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) | |
2 | pm2.61da2ne.2 | . . . 4 ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) | |
3 | 2 | adantlr 713 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 = 𝐷) → 𝜓) |
4 | pm2.61da2ne.3 | . . . 4 ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) | |
5 | 4 | anassrs 466 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ≠ 𝐷) → 𝜓) |
6 | 3, 5 | pm2.61dane 3025 | . 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) |
7 | 1, 6 | pm2.61dane 3025 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ≠ wne 2936 |
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-an 395 df-ne 2937 |
This theorem is referenced by: pm2.61da3ne 3027 isabvd 20705 xrsxmet 24743 chordthmlem3 26784 mumul 27131 lgsdirnn0 27295 lgsdinn0 27296 lfl1dim 38597 lfl1dim2N 38598 pmodlem2 39324 cdlemg29 40182 cdlemg39 40193 cdlemg44b 40209 dia2dimlem9 40549 dihprrn 40903 dvh3dim 40923 lcfl9a 40982 lclkrlem2l 40995 lcfrlem42 41061 mapdh6kN 41223 hdmap1l6k 41297 |
Copyright terms: Public domain | W3C validator |