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

Theorem sylan9eq 2168
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1 (𝜑𝐴 = 𝐵)
sylan9eq.2 (𝜓𝐵 = 𝐶)
Assertion
Ref Expression
sylan9eq ((𝜑𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2 (𝜑𝐴 = 𝐵)
2 sylan9eq.2 . 2 (𝜓𝐵 = 𝐶)
3 eqtr 2133 . 2 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
41, 2, 3syl2an 285 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  sylan9req  2169  sylan9eqr  2170  difeq12  3157  uneq12  3193  ineq12  3240  ifeq12  3456  preq12  3570  prprc  3601  preq12b  3665  opeq12  3675  xpeq12  4526  nfimad  4858  coi2  5023  funimass1  5168  f1orescnv  5349  resdif  5355  oveq12  5749  cbvmpov  5817  ovmpog  5871  eqopi  6036  fmpoco  6079  nnaordex  6389  map0g  6548  xpcomco  6686  xpmapenlem  6709  phplem3  6714  phplem4  6715  sbthlemi5  6815  addcmpblnq  7139  ltrnqg  7192  enq0ref  7205  addcmpblnq0  7215  distrlem4prl  7356  distrlem4pru  7357  recexgt0sr  7545  axcnre  7653  cnegexlem2  7902  cnegexlem3  7903  recexap  8374  xaddpnf2  9570  xaddmnf2  9572  rexadd  9575  xaddnemnf  9580  xaddnepnf  9581  xposdif  9605  frec2uzrand  10118  seqeq3  10163  shftcan1  10546  remul2  10585  immul2  10592  ef0lem  11265  efieq1re  11376  dvdsnegb  11406  dvdscmul  11416  dvds2ln  11422  dvds2add  11423  dvds2sub  11424  gcdn0val  11546  rpmulgcd  11610  lcmval  11640  lcmn0val  11643  isopn3  12189  dvexp  12718  dvexp2  12719  subctctexmid  12998
  Copyright terms: Public domain W3C validator