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

Theorem 3eqtr4d 2055
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4d.1 (φA = B)
3eqtr4d.2 (φ𝐶 = A)
3eqtr4d.3 (φ𝐷 = B)
Assertion
Ref Expression
3eqtr4d (φ𝐶 = 𝐷)

Proof of Theorem 3eqtr4d
StepHypRef Expression
1 3eqtr4d.2 . 2 (φ𝐶 = A)
2 3eqtr4d.3 . . 3 (φ𝐷 = B)
3 3eqtr4d.1 . . 3 (φA = B)
42, 3eqtr4d 2048 . 2 (φ𝐷 = A)
51, 4eqtr4d 2048 1 (φ𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1223
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 1309  ax-gen 1311  ax-4 1373  ax-17 1392  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-cleq 2006
This theorem is referenced by:  fnsnfv  5145  fvco2  5155  resfunexg  5295  fcof1  5336  fliftfun  5349  caovdir2d  5588  caov32d  5592  caov31d  5594  caov4d  5596  caovlem2d  5604  caofcom  5645  cnvf1olem  5756  tfrlem1  5833  tfrlemisucaccv  5848  frecrdg  5896  oav2  5946  omv2  5948  omsuc  5954  nnmsucr  5970  ecovicom  6113  ecoviass  6115  ecovidi  6117  addcompig  6175  addasspig  6176  mulcompig  6177  mulasspig  6178  distrpig  6179  addassnqg  6227  addnq0mo  6288  mulnq0mo  6289  nqnq0a  6295  nqnq0m  6296  distrnq0  6300  mulcomnq0  6301  addassnq0  6303  addcmpblnr  6477  mulcmpblnrlemg  6478  addsrmo  6481  mulsrmo  6482  ltsrprg  6485  recexgt0sr  6511  mulgt0sr  6514  mulextsr1lem  6516  addcnsrec  6548  mulcnsrec  6549  axaddcom  6559  adddir  6619  mul32  6743  mul31  6744  add32  6770  add4  6772  sub32  6844  sub4  6855  subdir  6982  mulneg2  6992  mulreim  7191  apadd1  7195  apneg  7198  divassap  7254  divdirap  7259  divmul13ap  7276  divmul24ap  7277  divdiv32ap  7281  conjmulap  7290  zeo  7907
  Copyright terms: Public domain W3C validator