![]() |
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 715 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 = 𝐷) → 𝜓) |
4 | pm2.61da2ne.3 | . . . 4 ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) | |
5 | 4 | anassrs 467 | . . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ≠ 𝐷) → 𝜓) |
6 | 3, 5 | pm2.61dane 3027 | . 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) |
7 | 1, 6 | pm2.61dane 3027 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ≠ wne 2938 |
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 207 df-an 396 df-ne 2939 |
This theorem is referenced by: pm2.61da3ne 3029 isabvd 20830 xrsxmet 24845 chordthmlem3 26892 mumul 27239 lgsdirnn0 27403 lgsdinn0 27404 constrrtcc 33741 lfl1dim 39103 lfl1dim2N 39104 pmodlem2 39830 cdlemg29 40688 cdlemg39 40699 cdlemg44b 40715 dia2dimlem9 41055 dihprrn 41409 dvh3dim 41429 lcfl9a 41488 lclkrlem2l 41501 lcfrlem42 41567 mapdh6kN 41729 hdmap1l6k 41803 |
Copyright terms: Public domain | W3C validator |