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

Theorem 3eqtr4d 2124
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 2117 . 2 (𝜑𝐷 = 𝐴)
51, 4eqtr4d 2117 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  fnsnfv  5258  fvco2  5268  resfunexg  5408  fcof1  5448  fliftfun  5461  caovdir2d  5702  caov32d  5706  caov31d  5708  caov4d  5710  caovlem2d  5718  caofcom  5759  cnvf1olem  5870  tfrlem1  5951  tfrlemisucaccv  5968  tfr1onlemsucaccv  5984  tfrcllemsucaccv  5997  frecrdg  6051  oav2  6101  omv2  6103  omsuc  6109  nnmsucr  6125  ecovicom  6273  ecoviass  6275  ecovidi  6277  carden2bex  6507  addcompig  6570  addasspig  6571  mulcompig  6572  mulasspig  6573  distrpig  6574  addassnqg  6623  addnq0mo  6688  mulnq0mo  6689  nqnq0a  6695  nqnq0m  6696  distrnq0  6700  mulcomnq0  6701  addassnq0  6703  addcmpblnr  6967  mulcmpblnrlemg  6968  addsrmo  6971  mulsrmo  6972  ltsrprg  6975  recexgt0sr  7001  mulgt0sr  7005  mulextsr1lem  7007  addcnsrec  7061  mulcnsrec  7062  pitonnlem2  7066  recidpirqlemcalc  7076  axaddcom  7087  adddir  7161  mul32  7294  mul31  7295  add32  7323  add4  7325  sub32  7398  sub4  7409  subdir  7546  mulneg2  7556  mulreim  7760  apadd1  7764  apneg  7767  divassap  7834  divdirap  7841  divmul13ap  7859  divmul24ap  7860  divdiv32ap  7864  conjmulap  7873  zeo  8522  lincmb01cmp  9090  iccf1o  9091  flhalf  9373  modqvalp1  9414  modqdi  9463  modqsubdir  9464  frecuzrdgg  9487  iseqshft2  9537  iseqcaopr3  9545  iseqcaopr  9547  iseqhomo  9554  iseqdistr  9556  expp1  9569  expnegap0  9570  expaddzaplem  9605  expaddzap  9606  expmulzap  9608  sqneg  9621  sqdivap  9626  subsq2  9668  binom2  9671  facp1  9743  bcm1k  9773  bcp1n  9774  ibcval5  9776  omgadd  9815  sizeun  9818  shftfibg  9835  shftfib  9838  shftval  9840  2shfti  9846  crre  9871  remim  9874  mulreap  9878  reneg  9882  readd  9883  remullem  9885  redivap  9888  imneg  9890  imadd  9891  imdivap  9895  cjcj  9897  cjadd  9898  cjmulrcl  9901  cjneg  9904  imval2  9908  resqrexlemcalc1  10027  absneg  10063  sqabsadd  10068  sqabssub  10069  absmul  10082  absresq  10091  absexp  10092  absexpzap  10093  serif0  10316  odd2np1lem  10405  oexpneg  10410  neggcd  10507  gcdabs2  10514  mulgcd  10538  mulgcdr  10540  gcddiv  10541  rplpwr  10549  eucalgval  10569  eucalginv  10571  eucialg  10574  neglcm  10590  lcmgcd  10593  mulgcddvds  10609  qredeu  10612
  Copyright terms: Public domain W3C validator