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

Theorem syl6eqr 2106
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 2060 . 2 𝐵 = 𝐶
41, 3syl6eq 2104 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  3eqtr4g  2113  rabxmdc  3277  relop  4514  csbcnvg  4547  dfiun3g  4617  dfiin3g  4618  resima2  4672  relcnvfld  4879  uniabio  4905  fntpg  4983  dffn5im  5247  dfimafn2  5251  fncnvima2  5316  fmptcof  5359  fcoconst  5362  fnasrng  5371  ffnov  5633  fnovim  5637  fnrnov  5674  foov  5675  funimassov  5678  ovelimab  5679  ofc12  5759  caofinvl  5761  dftpos3  5908  tfr0  5968  rdgisucinc  6003  oasuc  6075  ecinxp  6212  phplem1  6346  indpi  6498  nqnq0pi  6594  nq0m0r  6612  addnqpr1  6718  recexgt0sr  6916  recidpipr  6990  recidpirq  6992  axrnegex  7011  nntopi  7026  cnref1o  8680  fztp  9042  fseq1m1p1  9059  frecuzrdgrrn  9358  frecuzrdgsuc  9365  mulexpzap  9460  expaddzap  9464  bcp1m1  9633  cjexp  9721  rexuz3  9817  climconst  10042
  Copyright terms: Public domain W3C validator