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

Theorem syl6eqr 2090
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eqr.1 (𝜑𝐴 = 𝐵)
syl6eqr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6eqr (𝜑𝐴 = 𝐶)

Proof of Theorem syl6eqr
StepHypRef Expression
1 syl6eqr.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2044 . 2 𝐵 = 𝐶
41, 3syl6eq 2088 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  3eqtr4g  2097  rabxmdc  3249  relop  4486  csbcnvg  4519  dfiun3g  4589  dfiin3g  4590  resima2  4644  relcnvfld  4851  uniabio  4877  fntpg  4955  dffn5im  5219  dfimafn2  5223  fncnvima2  5288  fmptcof  5331  fcoconst  5334  fnasrng  5343  ffnov  5605  fnovim  5609  fnrnov  5646  foov  5647  funimassov  5650  ovelimab  5651  ofc12  5731  caofinvl  5733  dftpos3  5877  tfr0  5937  rdgisucinc  5972  oasuc  6044  ecinxp  6181  phplem1  6315  indpi  6438  nqnq0pi  6534  nq0m0r  6552  addnqpr1  6658  recexgt0sr  6856  recidpipr  6930  recidpirq  6932  axrnegex  6951  nntopi  6966  cnref1o  8580  fztp  8938  fseq1m1p1  8955  frecuzrdgrrn  9168  frecuzrdgsuc  9175  mulexpzap  9269  expaddzap  9273  cjexp  9467  rexuz3  9562  climconst  9784
  Copyright terms: Public domain W3C validator