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

Theorem ineq1d 3327
Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
ineq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ineq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem ineq1d
StepHypRef Expression
1 ineq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ineq1 3321 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  cin 3120
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-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  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-nfc 2301  df-v 2732  df-in 3127
This theorem is referenced by:  diftpsn3  3719  disji2  3980  ordpwsucexmid  4552  riinint  4870  fnresdisj  5306  fnimadisj  5316  ecinxp  6586  fiintim  6904  fival  6945  fzval2  9961  fvinim0ffz  10190  fsum1p  11374  fprod1p  11555  restopnb  12940  metrest  13265  qtopbasss  13280
  Copyright terms: Public domain W3C validator