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

Theorem 3eqtr4d 2098
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4d.1  |-  ( ph  ->  A  =  B )
3eqtr4d.2  |-  ( ph  ->  C  =  A )
3eqtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4d  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4d
StepHypRef Expression
1 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
2 3eqtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
3 3eqtr4d.1 . . 3  |-  ( ph  ->  A  =  B )
42, 3eqtr4d 2091 . 2  |-  ( ph  ->  D  =  A )
51, 4eqtr4d 2091 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:  fnsnfv  5260  fvco2  5270  resfunexg  5410  fcof1  5451  fliftfun  5464  caovdir2d  5705  caov32d  5709  caov31d  5711  caov4d  5713  caovlem2d  5721  caofcom  5762  cnvf1olem  5873  tfrlem1  5954  tfrlemisucaccv  5970  frecrdg  6023  oav2  6074  omv2  6076  omsuc  6082  nnmsucr  6098  ecovicom  6245  ecoviass  6247  ecovidi  6249  carden2bex  6427  addcompig  6485  addasspig  6486  mulcompig  6487  mulasspig  6488  distrpig  6489  addassnqg  6538  addnq0mo  6603  mulnq0mo  6604  nqnq0a  6610  nqnq0m  6611  distrnq0  6615  mulcomnq0  6616  addassnq0  6618  addcmpblnr  6882  mulcmpblnrlemg  6883  addsrmo  6886  mulsrmo  6887  ltsrprg  6890  recexgt0sr  6916  mulgt0sr  6920  mulextsr1lem  6922  addcnsrec  6976  mulcnsrec  6977  pitonnlem2  6981  recidpirqlemcalc  6991  axaddcom  7002  adddir  7076  mul32  7204  mul31  7205  add32  7233  add4  7235  sub32  7308  sub4  7319  subdir  7455  mulneg2  7465  mulreim  7669  apadd1  7673  apneg  7676  divassap  7743  divdirap  7748  divmul13ap  7766  divmul24ap  7767  divdiv32ap  7771  conjmulap  7780  zeo  8402  lincmb01cmp  8972  iccf1o  8973  flhalf  9252  modqvalp1  9293  modqdi  9342  modqsubdir  9343  iseqshft2  9396  iseqcaopr3  9404  iseqcaopr  9406  iseqhomo  9412  iseqdistr  9414  expp1  9427  expnegap0  9428  expaddzaplem  9463  expaddzap  9464  expmulzap  9466  sqneg  9479  sqdivap  9484  subsq2  9526  binom2  9529  facp1  9598  bcm1k  9628  bcp1n  9629  ibcval5  9631  shftfibg  9649  shftfib  9652  shftval  9654  2shfti  9660  crre  9685  remim  9688  mulreap  9692  reneg  9696  readd  9697  remullem  9699  redivap  9702  imneg  9704  imadd  9705  imdivap  9709  cjcj  9711  cjadd  9712  cjmulrcl  9715  cjneg  9718  imval2  9722  resqrexlemcalc1  9841  absneg  9877  sqabsadd  9882  sqabssub  9883  absmul  9896  absresq  9905  absexp  9906  absexpzap  9907  serif0  10102  odd2np1lem  10183  oexpneg  10188
  Copyright terms: Public domain W3C validator