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  6416  distrnq0  6441  distnq0r  6445  addnqprl  6511  addnqpru  6512  appdivnq  6543  ltmprr  6613  addcmpblnr  6647  mulcmpblnrlemg  6648  ltsrprg  6655  1idsr  6676  pn0sr  6679  mulgt0sr  6684  axmulass  6737  ax0id  6742  mul12  6919  mul4  6922  readdcan  6930  add12  6946  cnegexlem2  6964  addcan  6968  ppncan  7029  addsub4  7030  muladd  7157  mulcanapd  7404  receuap  7412  div13ap  7434  divdivdivap  7451  divcanap5  7452  divdivap1  7461  divdivap2  7462  halfaddsub  7916  fztp  8690  fseq1p1m1  8706  exprecap  8930  expsubap  8936  zesq  9000  crre  9065  resub  9078  imsub  9086  cjsub  9100
  Copyright terms: Public domain W3C validator