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

Theorem eqtr2di 2204
 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 2203 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2160 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332 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 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-cleq 2147 This theorem is referenced by:  eqtr4id  2206  elxp4  5066  elxp5  5067  fo1stresm  6099  fo2ndresm  6100  eloprabi  6134  fo2ndf  6164  xpsnen  6755  xpassen  6764  ac6sfi  6832  undifdc  6857  ine0  8248  nn0n0n1ge2  9213  fzval2  9893  fseq1p1m1  9974  fsum2dlemstep  11308  modfsummodlemstep  11331  fprod2dlemstep  11496  ef4p  11568  sin01bnd  11631  odd2np1  11737  sqpweven  12021  2sqpwodd  12022  psmetdmdm  12671  xmetdmdm  12703  dveflem  13034  reeff1oleme  13040  abssinper  13114
 Copyright terms: Public domain W3C validator