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

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

Proof of Theorem syl5reqr
StepHypRef Expression
1 syl5reqr.1 . . 3 𝐵 = 𝐴
21eqcomi 2092 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2133 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:  bm2.5ii  4303  resdmdfsn  4742  f0dom0  5188  f1o00  5272  fmpt  5433  fmptsn  5470  resfunexg  5500  mapsn  6427  sbthlemi4  6648  sbthlemi6  6650  pm54.43  6797  prarloclem5  7038  recexprlem1ssl  7171  recexprlem1ssu  7172  iooval2  9302  hashsng  10171  zfz1isolem1  10210  resqrexlemover  10408  isumclim3  10780
  Copyright terms: Public domain W3C validator