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

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

Proof of Theorem 3eqtr4d
StepHypRef Expression
1 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
2 3eqtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
3 3eqtr4d.1 . . 3 (𝜑𝐴 = 𝐵)
42, 3eqtr4d 2075 . 2 (𝜑𝐷 = 𝐴)
51, 4eqtr4d 2075 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:  fnsnfv  5219  fvco2  5229  resfunexg  5369  fcof1  5410  fliftfun  5423  caovdir2d  5664  caov32d  5668  caov31d  5670  caov4d  5672  caovlem2d  5680  caofcom  5721  cnvf1olem  5832  tfrlem1  5910  tfrlemisucaccv  5926  frecrdg  5979  oav2  6030  omv2  6032  omsuc  6038  nnmsucr  6054  ecovicom  6201  ecoviass  6203  ecovidi  6205  carden2bex  6350  addcompig  6408  addasspig  6409  mulcompig  6410  mulasspig  6411  distrpig  6412  addassnqg  6461  addnq0mo  6526  mulnq0mo  6527  nqnq0a  6533  nqnq0m  6534  distrnq0  6538  mulcomnq0  6539  addassnq0  6541  addcmpblnr  6805  mulcmpblnrlemg  6806  addsrmo  6809  mulsrmo  6810  ltsrprg  6813  recexgt0sr  6839  mulgt0sr  6843  mulextsr1lem  6845  addcnsrec  6899  mulcnsrec  6900  pitonnlem2  6904  recidpirqlemcalc  6914  axaddcom  6925  adddir  6999  mul32  7123  mul31  7124  add32  7150  add4  7152  sub32  7224  sub4  7235  subdir  7362  mulneg2  7372  mulreim  7571  apadd1  7575  apneg  7578  divassap  7645  divdirap  7650  divmul13ap  7667  divmul24ap  7668  divdiv32ap  7672  conjmulap  7681  zeo  8315  lincmb01cmp  8838  iccf1o  8839  iseqshft2  9110  iseqcaopr3  9118  iseqcaopr  9120  iseqhomo  9126  iseqdistr  9127  expp1  9140  expnegap0  9141  expaddzaplem  9176  expaddzap  9177  expmulzap  9179  sqneg  9191  sqdivap  9196  subsq2  9237  binom2  9240  shftfibg  9299  shftfib  9302  shftval  9304  2shfti  9310  crre  9335  remim  9338  mulreap  9342  reneg  9346  readd  9347  remullem  9349  redivap  9352  imneg  9354  imadd  9355  imdivap  9359  cjcj  9361  cjadd  9362  cjmulrcl  9365  cjneg  9368  imval2  9372  resqrexlemcalc1  9490  absneg  9526  sqabsadd  9531  sqabssub  9532  absmul  9545  absresq  9552  absexp  9553  absexpzap  9554  serif0  9748
  Copyright terms: Public domain W3C validator