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

Theorem eqtr2i 2103
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 2102 . 2  |-  A  =  C
43eqcomi 2086 1  |-  C  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  3eqtrri  2107  3eqtr2ri  2109  symdif1  3230  dfif3  3366  dfsn2  3414  prprc1  3502  ruv  4295  xpindi  4493  xpindir  4494  dmcnvcnv  4580  rncnvcnv  4581  imainrect  4790  dfrn4  4805  fcoi1  5095  foimacnv  5169  fsnunfv  5389  dfoprab3  5842  pitonnlem1  7064  ixi  7739  recexaplem2  7798  zeo  8522  num0h  8558  dec10p  8589  fseq1p1m1  9176  3lcm2e6woprm  10601
  Copyright terms: Public domain W3C validator