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

Theorem 3eqtr4rd 2083
 Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
Hypotheses
Ref Expression
3eqtr4d.1 (𝜑𝐴 = 𝐵)
3eqtr4d.2 (𝜑𝐶 = 𝐴)
3eqtr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3eqtr4rd (𝜑𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd
StepHypRef Expression
1 3eqtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
2 3eqtr4d.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2eqtr4d 2075 . 2 (𝜑𝐷 = 𝐴)
4 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
53, 4eqtr4d 2075 1 (𝜑𝐷 = 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1243 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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  csbcnvg  4519  phplem4  6318  phplem4on  6329  recexnq  6488  prarloclemcalc  6600  addcomprg  6676  mulcomprg  6678  mulcmpblnrlemg  6825  axmulass  6947  divnegap  7683  modqlt  9175  modqmulnn  9184  iseqcaopr3  9240  cjreb  9466  recj  9467  imcj  9475  imval2  9494  resqrexlemover  9608  sqrtmul  9633  amgm2  9714
 Copyright terms: Public domain W3C validator