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

Theorem eqtr3i 2105
 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 2087 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2103 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 2065 This theorem depends on definitions:  df-bi 115  df-cleq 2076 This theorem is referenced by:  3eqtr3i  2111  3eqtr3ri  2112  unundi  3144  unundir  3145  inindi  3200  inindir  3201  difun1  3241  difabs  3245  notab  3251  dfrab2  3256  dif0  3331  difdifdirss  3344  tpidm13  3511  intmin2  3683  univ  4254  iunxpconst  4447  dmres  4681  opabresid  4710  rnresi  4733  cnvcnv  4824  rnresv  4831  cnvsn0  4840  cnvsn  4854  resdmres  4863  coi2  4888  coires1  4889  dfdm2  4903  isarep2  5038  ssimaex  5288  fnreseql  5331  fmptpr  5409  idref  5450  mpt2mpt  5649  caov31  5743  xpexgALT  5813  cnvoprab  5908  frec0g  6068  unfiin  6472  xpfi  6474  djuin  6563  halfnqq  6739  caucvgprlemm  6997  caucvgprprlemmu  7024  caucvgsr  7117  mvlladdi  7470  8th4div3  8394  nneoor  8607  nummac  8679  numadd  8681  numaddc  8682  nummul1c  8683  decbin0  8774  infrenegsupex  8840  iseqvalcbv  9608  m1expcl2  9672  facnn  9828  fac0  9829  4bc3eq4  9874  fihasheq0  9895  resqrexlemcalc1  10126  sqrt1  10158  sqrt4  10159  sqrt9  10160  flodddiv4  10566  2prm  10741  znnen  10843
 Copyright terms: Public domain W3C validator