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  5167  elxp5  5168  fo1stresm  6237  fo2ndresm  6238  eloprabi  6272  fo2ndf  6303  xpsnen  6898  xpassen  6907  ac6sfi  6977  undifdc  7003  ine0  8448  nn0n0n1ge2  9425  fzval2  10115  fseq1p1m1  10198  fsum2dlemstep  11664  modfsummodlemstep  11687  fprod2dlemstep  11852  ef4p  11924  sin01bnd  11987  odd2np1  12103  sqpweven  12416  2sqpwodd  12417  psmetdmdm  14714  xmetdmdm  14746  dveflem  15116  reeff1oleme  15162  abssinper  15236  lgseisenlem1  15465
  Copyright terms: Public domain W3C validator