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

Theorem eqtr2di 2216
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
eqtr2di.1  |-  ( ph  ->  A  =  B )
eqtr2di.2  |-  B  =  C
Assertion
Ref Expression
eqtr2di  |-  ( ph  ->  C  =  A )

Proof of Theorem eqtr2di
StepHypRef Expression
1 eqtr2di.1 . . 3  |-  ( ph  ->  A  =  B )
2 eqtr2di.2 . . 3  |-  B  =  C
31, 2eqtrdi 2215 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2171 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1343
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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147
This theorem depends on definitions:  df-bi 116  df-cleq 2158
This theorem is referenced by:  eqtr4id  2218  elxp4  5091  elxp5  5092  fo1stresm  6129  fo2ndresm  6130  eloprabi  6164  fo2ndf  6195  xpsnen  6787  xpassen  6796  ac6sfi  6864  undifdc  6889  ine0  8292  nn0n0n1ge2  9261  fzval2  9947  fseq1p1m1  10029  fsum2dlemstep  11375  modfsummodlemstep  11398  fprod2dlemstep  11563  ef4p  11635  sin01bnd  11698  odd2np1  11810  sqpweven  12107  2sqpwodd  12108  psmetdmdm  12964  xmetdmdm  12996  dveflem  13327  reeff1oleme  13333  abssinper  13407
  Copyright terms: Public domain W3C validator