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

Theorem syl5eqr 2131
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 2089 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2129 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  3eqtr3g  2140  csbeq1a  2930  ssdifeq0  3352  pofun  4113  opabbi2dv  4553  funimaexg  5063  fresin  5152  f1imacnv  5233  foimacnv  5234  fsn2  5434  fmptpr  5452  funiunfvdm  5503  funiunfvdmf  5504  fcof1o  5529  f1opw2  5807  fnexALT  5841  eqerlem  6275  pmresg  6385  mapsn  6399  fopwdom  6504  mapen  6514  xpfi  6590  sbthlemi8  6617  sbthlemi9  6618  exmidfodomrlemim  6771  mul02  7809  recdivap  8124  fzpreddisj  9415  fzshftral  9452  qbtwnrelemcalc  9595  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  binom3  9967  bcn2  10068  hashfz1  10087  hashunlem  10108  hashfacen  10137  cnrecnv  10239  resqrexlemnm  10346  amgm2  10446  fisumss  10670  dfgcd3  10874  eucalgval  10911  sqrt2irrlem  11015  nninfsellemqall  11345
  Copyright terms: Public domain W3C validator