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

Theorem syl6reqr 2139
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6reqr.1 (𝜑𝐴 = 𝐵)
syl6reqr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6reqr (𝜑𝐶 = 𝐴)

Proof of Theorem syl6reqr
StepHypRef Expression
1 syl6reqr.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6reqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2092 . 2 𝐵 = 𝐶
41, 3syl6req 2137 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289
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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  iftrue  3398  iffalse  3401  difprsn1  3576  dmmptg  4928  relcoi1  4962  funimacnv  5090  dffv3g  5301  dfimafn  5353  fvco2  5373  isoini  5597  oprabco  5982  unfiexmid  6628  undifdc  6634  sbthlemi4  6669  sbthlemi5  6670  sbthlemi6  6671  supval2ti  6690  exmidfodomrlemim  6827  eqneg  8199  zeo  8851  fseq1p1m1  9508  iseqval  9871  iseqvalt  9873  seq3val  9874  hashfzo  10230  hashxp  10234  fsumconst  10848  modfsummod  10852  telfsumo  10860  mulgcd  11283  ialgrp1  11306  ialgcvg  11308  phiprmpw  11476  strslfv3  11539
  Copyright terms: Public domain W3C validator