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

Theorem syl6eqr 2135
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 2089 . 2 𝐵 = 𝐶
41, 3syl6eq 2133 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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:  3eqtr4g  2142  rabxmdc  3303  relop  4553  csbcnvg  4587  dfiun3g  4657  dfiin3g  4658  resima2  4712  relcnvfld  4927  uniabio  4953  fntpg  5032  dffn5im  5307  dfimafn2  5311  fncnvima2  5377  fmptcof  5422  fcoconst  5425  fnasrng  5434  ffnov  5700  fnovim  5704  fnrnov  5741  foov  5742  funimassov  5745  ovelimab  5746  ofc12  5826  caofinvl  5828  dftpos3  5975  tfr0dm  6035  rdgisucinc  6098  oasuc  6173  ecinxp  6313  phplem1  6514  exmidpw  6570  unfiin  6582  indpi  6838  nqnq0pi  6934  nq0m0r  6952  addnqpr1  7058  recexgt0sr  7256  recidpipr  7330  recidpirq  7332  axrnegex  7351  nntopi  7366  cnref1o  9058  fztp  9415  fseq1m1p1  9432  frecuzrdgrrn  9736  frecuzrdgsuc  9742  frecuzrdgsuctlem  9751  iseqvalt  9783  fser0const  9842  mulexpzap  9886  expaddzap  9890  bcp1m1  10062  cjexp  10215  rexuz3  10311  climconst  10564  sumfct  10646  zisum  10656  fisum  10658  sum0  10659  eucalgval  10903  eucalginv  10905  eucalglt  10906  eucialgcvga  10907  eucialg  10908  sqpweven  11020  2sqpwodd  11021  dfphi2  11063  phimullem  11068  nninfsellemqall  11337
  Copyright terms: Public domain W3C validator