ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan9eq Structured version   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  6415  addcmpblnq0  6425  distrlem4prl  6559  distrlem4pru  6560  recexgt0sr  6681  axcnre  6745  cnegexlem2  6964  cnegexlem3  6965  recexap  7396  frec2uzzd  8847  frec2uzrand  8852  iseqeq3  8876  remul2  9081  immul2  9088
  Copyright terms: Public domain W3C validator