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