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

Theorem 3eqtr4rd 2126
 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 2118 . 2 (𝜑𝐷 = 𝐴)
4 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
53, 4eqtr4d 2118 1 (𝜑𝐷 = 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1285 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065 This theorem depends on definitions:  df-bi 115  df-cleq 2076 This theorem is referenced by:  csbcnvg  4567  phplem4  6411  phplem4on  6423  recexnq  6694  prarloclemcalc  6806  addcomprg  6882  mulcomprg  6884  mulcmpblnrlemg  7031  axmulass  7153  divnegap  7913  modqlt  9467  modqmulnn  9476  iseqvalt  9584  iseqcaopr3  9608  ibcval5  9839  omgadd  9878  cjreb  9954  recj  9955  imcj  9963  imval2  9982  resqrexlemover  10097  sqrtmul  10122  amgm2  10205  maxabslemab  10293  flodddiv4  10541  dfgcd3  10606  absmulgcd  10613  sqpweven  10760  2sqpwodd  10761  crth  10807
 Copyright terms: Public domain W3C validator