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

Theorem eqtr2i 2103
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1 𝐴 = 𝐵
eqtr2i.2 𝐵 = 𝐶
Assertion
Ref Expression
eqtr2i 𝐶 = 𝐴

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3 𝐴 = 𝐵
2 eqtr2i.2 . . 3 𝐵 = 𝐶
31, 2eqtri 2102 . 2 𝐴 = 𝐶
43eqcomi 2086 1 𝐶 = 𝐴
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  3236  dfif3  3372  dfsn2  3420  prprc1  3508  ruv  4301  xpindi  4499  xpindir  4500  dmcnvcnv  4586  rncnvcnv  4587  imainrect  4796  dfrn4  4811  fcoi1  5101  foimacnv  5175  fsnunfv  5395  dfoprab3  5848  pitonnlem1  7075  ixi  7750  recexaplem2  7809  zeo  8533  num0h  8569  dec10p  8600  fseq1p1m1  9187  3lcm2e6woprm  10612
  Copyright terms: Public domain W3C validator