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

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

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (φA = B)
2 3eqtr3d.2 . . 3 (φA = 𝐶)
31, 2eqtr3d 2071 . 2 (φB = 𝐶)
4 3eqtr3d.3 . 2 (φB = 𝐷)
53, 4eqtr3d 2071 1 (φ𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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:  mpteqb  5204  fvmptt  5205  fsnunfv  5306  f1ocnvfv1  5360  f1ocnvfv2  5361  fcof1  5366  caov12d  5624  caov13d  5626  caov411d  5628  caovimo  5636  grprinvlem  5637  grprinvd  5638  grpridd  5639  tfrlem5  5871  tfrlemiubacc  5885  nndir  6008  fopwdom  6246  addassnqg  6366  distrnqg  6371  enq0tr  6417  distrnq0  6442  distnq0r  6446  addnqprl  6512  addnqpru  6513  appdivnq  6544  ltmprr  6614  addcmpblnr  6667  mulcmpblnrlemg  6668  ltsrprg  6675  1idsr  6696  pn0sr  6699  mulgt0sr  6704  axmulass  6757  ax0id  6762  mul12  6939  mul4  6942  readdcan  6950  add12  6966  cnegexlem2  6984  addcan  6988  ppncan  7049  addsub4  7050  muladd  7177  mulcanapd  7424  receuap  7432  div13ap  7454  divdivdivap  7471  divcanap5  7472  divdivap1  7481  divdivap2  7482  halfaddsub  7936  fztp  8710  fseq1p1m1  8726  exprecap  8950  expsubap  8956  zesq  9020  crre  9085  resub  9098  imsub  9106  cjsub  9120
  Copyright terms: Public domain W3C validator