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 747 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 = 𝐷) → 𝜓) |
4 | pm2.61da2ne.3 | . . . 4 ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) | |
5 | 4 | anassrs 678 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ≠ 𝐷) → 𝜓) |
6 | 3, 5 | pm2.61dane 2869 | . 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) |
7 | 1, 6 | pm2.61dane 2869 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ≠ wne 2780 |
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 196 df-an 385 df-ne 2782 |
This theorem is referenced by: pm2.61da3ne 2871 isabvd 18643 xrsxmet 22420 chordthmlem3 24361 mumul 24707 lgsdirnn0 24869 lgsdinn0 24870 eupath2lem3 26506 lfl1dim 33426 lfl1dim2N 33427 pmodlem2 34151 cdlemg29 35011 cdlemg39 35022 cdlemg44b 35038 dia2dimlem9 35379 dihprrn 35733 dvh3dim 35753 lcfl9a 35812 lclkrlem2l 35825 lcfrlem42 35891 mapdh6kN 36053 hdmap1l6k 36128 |
Copyright terms: Public domain | W3C validator |