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

Theorem syl5eqr 2102
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eqr.1 𝐵 = 𝐴
syl5eqr.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
syl5eqr (𝜑𝐴 = 𝐶)

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3 𝐵 = 𝐴
21eqcomi 2060 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2100 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:  3eqtr3g  2111  csbeq1a  2888  ssdifeq0  3333  pofun  4077  opabbi2dv  4513  funimaexg  5011  fresin  5096  f1imacnv  5171  foimacnv  5172  fsn2  5365  fmptpr  5383  funiunfvdm  5430  funiunfvdmf  5431  fcof1o  5457  f1opw2  5734  fnexALT  5768  eqerlem  6168  fopwdom  6341  mul02  7456  recdivap  7769  fzpreddisj  9035  fzshftral  9072  qbtwnrelemcalc  9212  frec2uzrdg  9359  binom3  9534  bcn2  9632  cnrecnv  9738  resqrexlemnm  9845  amgm2  9945  sqr2irrlem  10250
  Copyright terms: Public domain W3C validator