|   | 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 3029 | . 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) | 
| 7 | 1, 6 | pm2.61dane 3029 | 1 ⊢ (𝜑 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ≠ 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 207 df-an 396 df-ne 2941 | 
| This theorem is referenced by: pm2.61da3ne 3031 isabvd 20813 xrsxmet 24831 chordthmlem3 26877 mumul 27224 lgsdirnn0 27388 lgsdinn0 27389 constrrtcc 33776 lfl1dim 39122 lfl1dim2N 39123 pmodlem2 39849 cdlemg29 40707 cdlemg39 40718 cdlemg44b 40734 dia2dimlem9 41074 dihprrn 41428 dvh3dim 41448 lcfl9a 41507 lclkrlem2l 41520 lcfrlem42 41586 mapdh6kN 41748 hdmap1l6k 41822 | 
| Copyright terms: Public domain | W3C validator |