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

Theorem eqtr2i 2137
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1  |-  A  =  B
eqtr2i.2  |-  B  =  C
Assertion
Ref Expression
eqtr2i  |-  C  =  A

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3  |-  A  =  B
2 eqtr2i.2 . . 3  |-  B  =  C
31, 2eqtri 2136 . 2  |-  A  =  C
43eqcomi 2119 1  |-  C  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1314
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  3eqtrri  2141  3eqtr2ri  2143  symdif1  3309  dfif3  3455  dfsn2  3509  prprc1  3599  ruv  4433  xpindi  4642  xpindir  4643  dmcnvcnv  4731  rncnvcnv  4732  imainrect  4952  dfrn4  4967  fcoi1  5271  foimacnv  5351  fsnunfv  5587  dfoprab3  6055  fiintim  6783  sbthlemi8  6818  pitonnlem1  7617  ixi  8308  recexaplem2  8376  zeo  9110  num0h  9147  dec10p  9178  fseq1p1m1  9825  fsumrelem  11191  ef0lem  11276  ef01bndlem  11373  3lcm2e6woprm  11674  strsl0  11913  tgioo  12621  tgqioo  12622  dveflem  12761
  Copyright terms: Public domain W3C validator