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

Theorem eqtr2id 2217
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
eqtr2id.1 𝐴 = 𝐵
eqtr2id.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eqtr2id (𝜑𝐶 = 𝐴)

Proof of Theorem eqtr2id
StepHypRef Expression
1 eqtr2id.1 . . 3 𝐴 = 𝐵
2 eqtr2id.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrid 2216 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2177 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1349
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-5 1441  ax-gen 1443  ax-4 1504  ax-17 1520  ax-ext 2153
This theorem depends on definitions:  df-bi 116  df-cleq 2164
This theorem is referenced by:  eqtr3di  2219  opeqsn  4238  dcextest  4566  relop  4762  funopg  5234  funcnvres  5273  mapsnconst  6676  snexxph  6931  apreap  8510  recextlem1  8573  nn0supp  9191  intqfrac2  10279  hashprg  10747  hashfacen  10775  explecnv  11472  grp1inv  12810  rerestcntop  13429  binom4  13776
  Copyright terms: Public domain W3C validator