![]() |
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 471 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ≠ 𝐷) → 𝜓) |
6 | 3, 5 | pm2.61dane 3074 | . 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) |
7 | 1, 6 | pm2.61dane 3074 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ≠ wne 2987 |
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-an 400 df-ne 2988 |
This theorem is referenced by: pm2.61da3ne 3076 isabvd 19584 xrsxmet 23414 chordthmlem3 25420 mumul 25766 lgsdirnn0 25928 lgsdinn0 25929 lfl1dim 36417 lfl1dim2N 36418 pmodlem2 37143 cdlemg29 38001 cdlemg39 38012 cdlemg44b 38028 dia2dimlem9 38368 dihprrn 38722 dvh3dim 38742 lcfl9a 38801 lclkrlem2l 38814 lcfrlem42 38880 mapdh6kN 39042 hdmap1l6k 39116 |
Copyright terms: Public domain | W3C validator |