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

Theorem eqtr3i 2107
Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)
Hypotheses
Ref Expression
eqtr3i.1 𝐴 = 𝐵
eqtr3i.2 𝐴 = 𝐶
Assertion
Ref Expression
eqtr3i 𝐵 = 𝐶

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3 𝐴 = 𝐵
21eqcomi 2089 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2105 1 𝐵 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1287
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  3eqtr3i  2113  3eqtr3ri  2114  unundi  3150  unundir  3151  inindi  3206  inindir  3207  difun1  3248  difabs  3252  notab  3258  dfrab2  3263  dif0  3341  difdifdirss  3354  tpidm13  3527  intmin2  3699  univ  4273  iunxpconst  4468  dmres  4703  opabresid  4734  rnresi  4758  cnvcnv  4851  rnresv  4858  cnvsn0  4867  cnvsn  4881  resdmres  4890  coi2  4915  coires1  4916  dfdm2  4933  isarep2  5068  ssimaex  5330  fnreseql  5374  fmptpr  5454  idref  5499  mpt2mpt  5699  caov31  5793  xpexgALT  5863  cnvoprab  5958  frec0g  6118  unfiin  6590  xpfi  6593  djuin  6703  halfnqq  6916  caucvgprlemm  7174  caucvgprprlemmu  7201  caucvgsr  7294  mvlladdi  7647  8th4div3  8571  nneoor  8784  nummac  8856  numadd  8858  numaddc  8859  nummul1c  8860  decbin0  8951  infrenegsupex  9017  iseqvalcbv  9792  m1expcl2  9879  facnn  10035  fac0  10036  4bc3eq4  10081  fihasheq0  10102  resqrexlemcalc1  10346  sqrt1  10378  sqrt4  10379  sqrt9  10380  isumss2  10676  flodddiv4  10840  2prm  11015  znnen  11117
  Copyright terms: Public domain W3C validator