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

Theorem syl6reqr 2169
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 2121 . 2 𝐵 = 𝐶
41, 3syl6req 2167 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  iftrue  3449  iffalse  3452  difprsn1  3629  dmmptg  5006  relcoi1  5040  funimacnv  5169  dmmptd  5223  dffv3g  5385  dfimafn  5438  fvco2  5458  isoini  5687  oprabco  6082  ixpconstg  6569  unfiexmid  6774  undifdc  6780  sbthlemi4  6816  sbthlemi5  6817  sbthlemi6  6818  supval2ti  6850  exmidfodomrlemim  7025  suplocexprlemex  7498  eqneg  8460  zeo  9124  fseq1p1m1  9842  seq3val  10199  seqvalcd  10200  hashfzo  10536  hashxp  10540  fsumconst  11191  modfsummod  11195  telfsumo  11203  mulgcd  11631  algcvg  11656  phiprmpw  11825  strslfv3  11931  uptx  12370  resubmet  12644
  Copyright terms: Public domain W3C validator