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

Theorem 3eqtr3d 2096
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  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3d  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
31, 2eqtr3d 2090 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2090 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  mpteqb  5289  fvmptt  5290  fsnunfv  5391  f1ocnvfv1  5445  f1ocnvfv2  5446  fcof1  5451  caov12d  5710  caov13d  5712  caov411d  5714  caovimo  5722  grprinvlem  5723  grprinvd  5724  grpridd  5725  tfrlem5  5961  tfrlemiubacc  5975  nndir  6100  fopwdom  6341  addassnqg  6538  distrnqg  6543  enq0tr  6590  distrnq0  6615  distnq0r  6619  addnqprl  6685  addnqpru  6686  appdivnq  6719  ltmprr  6798  addcmpblnr  6882  mulcmpblnrlemg  6883  ltsrprg  6890  1idsr  6911  pn0sr  6914  mulgt0sr  6920  axmulass  7005  ax0id  7010  recriota  7022  mul12  7203  mul4  7206  readdcan  7214  add12  7232  cnegexlem2  7250  addcan  7254  ppncan  7316  addsub4  7317  subaddeqd  7439  muladd  7453  mulcanapd  7716  receuap  7724  div13ap  7746  divdivdivap  7764  divcanap5  7765  divdivap1  7774  divdivap2  7775  halfaddsub  8216  fztp  9042  fseq1p1m1  9058  flqzadd  9248  flqdiv  9271  mulp1mod1  9315  modqnegd  9329  modqsub12d  9331  q2submod  9335  modsumfzodifsn  9346  iseqm1  9391  iseqcaopr  9406  exprecap  9461  expsubap  9468  zesq  9535  nn0opthlem1d  9588  facnn2  9602  faclbnd6  9612  shftval3  9656  crre  9685  resub  9698  imsub  9706  cjsub  9720  climshft2  10058  qdencn  10511
  Copyright terms: Public domain W3C validator