ILE Home 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