|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > eqnetrrid | Structured version Visualization version GIF version | ||
| Description: A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) | 
| Ref | Expression | 
|---|---|
| eqnetrrid.1 | ⊢ 𝐵 = 𝐴 | 
| eqnetrrid.2 | ⊢ (𝜑 → 𝐵 ≠ 𝐶) | 
| Ref | Expression | 
|---|---|
| eqnetrrid | ⊢ (𝜑 → 𝐴 ≠ 𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqnetrrid.1 | . . 3 ⊢ 𝐵 = 𝐴 | |
| 2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) | 
| 3 | eqnetrrid.2 | . 2 ⊢ (𝜑 → 𝐵 ≠ 𝐶) | |
| 4 | 2, 3 | eqnetrrd 3008 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 ≠ wne 2939 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-ne 2940 | 
| This theorem is referenced by: xpcoidgend 15015 fclsfnflim 24036 ptcmplem2 24062 vieta1lem1 26353 vieta1lem2 26354 fsuppcurry1 32737 fsuppcurry2 32738 signsvfpn 34601 signsvfnn 34602 finxpreclem2 37392 finxp1o 37394 cdleme3h 40238 cdleme7ga 40251 imo72b2lem0 44183 imo72b2lem1 44187 fourierdlem42 46169 | 
| Copyright terms: Public domain | W3C validator |