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

Theorem syl6reqr 2107
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 2060 . 2 𝐵 = 𝐶
41, 3syl6req 2105 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:  iftrue  3364  iffalse  3367  difprsn1  3531  dmmptg  4846  relcoi1  4877  funimacnv  5003  dffv3g  5202  dfimafn  5250  fvco2  5270  isoini  5485  oprabco  5866  supval2ti  6401  eqneg  7783  zeo  8402  fseq1p1m1  9058  iseqval  9384  ialgrp1  10268  ialgcvg  10270
  Copyright terms: Public domain W3C validator