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

Theorem difeq2d 3245
Description: Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
difeq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem difeq2d
StepHypRef Expression
1 difeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 difeq2 3239 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  cdif 3118
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 609  ax-in2 610  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-ral 2453  df-rab 2457  df-dif 3123
This theorem is referenced by:  difeq12d  3246  phplem3  6832  phplem4  6833  phplem3g  6834  phplem4dom  6840  phplem4on  6845  fidifsnen  6848  xpfi  6907  sbthlem2  6935  sbthlemi3  6936  isbth  6944  ismkvnex  7131  setsvalg  12446  setsvala  12447  exmid1stab  14033
  Copyright terms: Public domain W3C validator