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

Theorem 3eqtr3d 2080
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 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3d (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
31, 2eqtr3d 2074 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2074 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:  mpteqb  5261  fvmptt  5262  fsnunfv  5363  f1ocnvfv1  5417  f1ocnvfv2  5418  fcof1  5423  caov12d  5682  caov13d  5684  caov411d  5686  caovimo  5694  grprinvlem  5695  grprinvd  5696  grpridd  5697  tfrlem5  5930  tfrlemiubacc  5944  nndir  6069  fopwdom  6310  addassnqg  6478  distrnqg  6483  enq0tr  6530  distrnq0  6555  distnq0r  6559  addnqprl  6625  addnqpru  6626  appdivnq  6659  ltmprr  6738  addcmpblnr  6822  mulcmpblnrlemg  6823  ltsrprg  6830  1idsr  6851  pn0sr  6854  mulgt0sr  6860  axmulass  6945  ax0id  6950  recriota  6962  mul12  7140  mul4  7143  readdcan  7151  add12  7167  cnegexlem2  7185  addcan  7189  ppncan  7251  addsub4  7252  muladd  7379  mulcanapd  7640  receuap  7648  div13ap  7670  divdivdivap  7687  divcanap5  7688  divdivap1  7697  divdivap2  7698  halfaddsub  8157  fztp  8938  fseq1p1m1  8954  flqzadd  9138  iseqm1  9201  iseqcaopr  9216  exprecap  9270  expsubap  9276  zesq  9341  shftval3  9402  crre  9431  resub  9444  imsub  9452  cjsub  9466  climshft2  9801
  Copyright terms: Public domain W3C validator