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

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

Proof of Theorem eqtr2id
StepHypRef Expression
1 eqtr2id.1 . . 3  |-  A  =  B
2 eqtr2id.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2eqtrid 2215 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2176 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1348
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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163
This theorem is referenced by:  eqtr3di  2218  opeqsn  4235  dcextest  4563  relop  4759  funopg  5230  funcnvres  5269  mapsnconst  6668  snexxph  6923  apreap  8493  recextlem1  8556  nn0supp  9174  intqfrac2  10262  hashprg  10730  hashfacen  10758  explecnv  11455  rerestcntop  13303  binom4  13650
  Copyright terms: Public domain W3C validator