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

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

Proof of Theorem eqtr2di
StepHypRef Expression
1 eqtr2di.1 . . 3 (𝜑𝐴 = 𝐵)
2 eqtr2di.2 . . 3 𝐵 = 𝐶
31, 2eqtrdi 2253 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2210 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186
This theorem depends on definitions:  df-bi 117  df-cleq 2197
This theorem is referenced by:  eqtr4id  2256  elxp4  5169  elxp5  5170  fo1stresm  6246  fo2ndresm  6247  eloprabi  6281  fo2ndf  6312  xpsnen  6915  xpassen  6924  ac6sfi  6994  undifdc  7020  ine0  8465  nn0n0n1ge2  9442  fzval2  10132  fseq1p1m1  10215  fsum2dlemstep  11687  modfsummodlemstep  11710  fprod2dlemstep  11875  ef4p  11947  sin01bnd  12010  odd2np1  12126  sqpweven  12439  2sqpwodd  12440  psmetdmdm  14738  xmetdmdm  14770  dveflem  15140  reeff1oleme  15186  abssinper  15260  lgseisenlem1  15489
  Copyright terms: Public domain W3C validator