Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  neeq1d GIF version

Theorem neeq1d 2327
 Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
Hypothesis
Ref Expression
neeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
neeq1d (𝜑 → (𝐴𝐶𝐵𝐶))

Proof of Theorem neeq1d
StepHypRef Expression
1 neeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 neeq1 2322 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐶𝐵𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ≠ wne 2309 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-ne 2310 This theorem is referenced by:  neeq12d  2329  eqnetrd  2333  prnzg  3651  hashprg  10582  algcvg  11756  algcvga  11759  eucalgcvga  11766  rpdvds  11807  phibndlem  11919  dfphi2  11923  ennnfoneleminc  11951  ennnfonelemex  11954  ennnfonelemhom  11955  ennnfonelemnn0  11962  ennnfonelemr  11963  ennnfonelemim  11964  ctinfomlemom  11967  dcapncf  13406
 Copyright terms: Public domain W3C validator