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

Theorem 3eqtr3d 2128
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 2122 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2122 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289
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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  mpteqb  5377  fvmptt  5378  fsnunfv  5481  f1ocnvfv1  5538  f1ocnvfv2  5539  fcof1  5544  caov12d  5808  caov13d  5810  caov411d  5812  caovimo  5820  grprinvlem  5821  grprinvd  5822  grpridd  5823  tfrlem5  6061  tfrlemiubacc  6077  tfr1onlemubacc  6093  tfrcllemubacc  6106  nndir  6233  fopwdom  6532  updjud  6752  addassnqg  6920  distrnqg  6925  enq0tr  6972  distrnq0  6997  distnq0r  7001  addnqprl  7067  addnqpru  7068  appdivnq  7101  ltmprr  7180  addcmpblnr  7264  mulcmpblnrlemg  7265  ltsrprg  7272  1idsr  7293  pn0sr  7296  mulgt0sr  7302  axmulass  7387  ax0id  7392  recriota  7404  mul12  7590  mul4  7593  readdcan  7601  add12  7619  cnegexlem2  7637  addcan  7641  ppncan  7703  addsub4  7704  subaddeqd  7826  muladd  7841  mulcanapd  8104  receuap  8112  div13ap  8134  divdivdivap  8154  divcanap5  8155  divdivap1  8164  divdivap2  8165  halfaddsub  8620  fztp  9459  fseq1p1m1  9475  flqzadd  9670  flqdiv  9693  mulp1mod1  9737  modqnegd  9751  modqsub12d  9753  q2submod  9757  modsumfzodifsn  9768  iseqm1  9853  seq3m1  9854  seq3feq  9862  seq3shft2  9864  iseqcaopr  9877  iseqf1olemab  9883  iseqf1olemnanb  9884  seq3f1olemqsumk  9893  ser3add  9900  exprecap  9961  expsubap  9968  zesq  10037  nn0opthlem1d  10093  facnn2  10107  faclbnd6  10117  zfz1isolemsplit  10208  iseqcoll  10212  shftval3  10226  crre  10256  resub  10269  imsub  10277  cjsub  10291  climshft2  10659  isummolemnm  10733  fsumf1o  10746  isumss  10747  fisumss  10748  fsumadd  10763  isumclim3  10780  fsummulc2  10805  fsumsub  10809  telfsumo  10823  telfsumo2  10824  hashiun  10834  bcxmas  10845  isumshft  10846  trireciplem  10855  geoserap  10862  geo2sum2  10870  gcdaddm  11068  modgcd  11075  bezoutlemnewy  11078  absmulgcd  11099  gcdmultiplez  11103  eucialg  11134  lcmgcd  11153  lcmid  11155  numdensq  11273  dfphi2  11289  phiprm  11292  hashgcdlem  11296  peano4nninf  11553  nninfalllem1  11556  nninfall  11557  nninfsellemqall  11564  qdencn  11572
  Copyright terms: Public domain W3C validator