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

Theorem sylan9eq 2089
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1 (φA = B)
sylan9eq.2 (ψB = 𝐶)
Assertion
Ref Expression
sylan9eq ((φ ψ) → A = 𝐶)

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2 (φA = B)
2 sylan9eq.2 . 2 (ψB = 𝐶)
3 eqtr 2054 . 2 ((A = B B = 𝐶) → A = 𝐶)
41, 2, 3syl2an 273 1 ((φ ψ) → A = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  sylan9req  2090  sylan9eqr  2091  difeq12  3051  uneq12  3086  ineq12  3127  ifeq12  3338  preq12  3440  prprc  3471  preq12b  3532  opeq12  3542  xpeq12  4307  nfimad  4620  coi2  4780  funimass1  4919  f1orescnv  5085  resdif  5091  oveq12  5464  cbvmpt2v  5526  ovmpt2g  5577  eqopi  5740  fmpt2co  5779  nnaordex  6036  xpcomco  6236  addcmpblnq  6351  ltrnqg  6403  enq0ref  6416  addcmpblnq0  6426  distrlem4prl  6560  distrlem4pru  6561  recexgt0sr  6701  axcnre  6765  cnegexlem2  6984  cnegexlem3  6985  recexap  7416  frec2uzzd  8867  frec2uzrand  8872  iseqeq3  8896  remul2  9101  immul2  9108
  Copyright terms: Public domain W3C validator