![]() |
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 714 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 = 𝐷) → 𝜓) |
4 | pm2.61da2ne.3 | . . . 4 ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) | |
5 | 4 | anassrs 469 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ≠ 𝐷) → 𝜓) |
6 | 3, 5 | pm2.61dane 3029 | . 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) |
7 | 1, 6 | pm2.61dane 3029 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ≠ wne 2940 |
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 398 df-ne 2941 |
This theorem is referenced by: pm2.61da3ne 3031 isabvd 20293 xrsxmet 24188 chordthmlem3 26200 mumul 26546 lgsdirnn0 26708 lgsdinn0 26709 lfl1dim 37629 lfl1dim2N 37630 pmodlem2 38356 cdlemg29 39214 cdlemg39 39225 cdlemg44b 39241 dia2dimlem9 39581 dihprrn 39935 dvh3dim 39955 lcfl9a 40014 lclkrlem2l 40027 lcfrlem42 40093 mapdh6kN 40255 hdmap1l6k 40329 |
Copyright terms: Public domain | W3C validator |