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

Theorem 3eqtr4i 2086
Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1  |-  A  =  B
3eqtr4i.2  |-  C  =  A
3eqtr4i.3  |-  D  =  B
Assertion
Ref Expression
3eqtr4i  |-  C  =  D

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2  |-  C  =  A
2 3eqtr4i.3 . . 3  |-  D  =  B
3 3eqtr4i.1 . . 3  |-  A  =  B
42, 3eqtr4i 2079 . 2  |-  D  =  A
51, 4eqtr4i 2079 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = 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:  rabswap  2505  rabbiia  2564  cbvrab  2572  cbvcsb  2883  csbco  2888  cbvrabcsf  2938  un4  3130  in13  3177  in31  3178  in4  3180  indifcom  3210  indir  3213  undir  3214  notrab  3241  dfnul3  3254  rab0  3273  prcom  3473  tprot  3490  tpcoma  3491  tpcomb  3492  tpass  3493  qdassr  3495  pw0  3538  opid  3594  int0  3656  cbviun  3721  cbviin  3722  iunrab  3731  iunin1  3748  cbvopab  3855  cbvopab1  3857  cbvopab2  3858  cbvopab1s  3859  cbvopab2v  3861  unopab  3863  cbvmpt  3878  iunopab  4045  uniuni  4210  2ordpr  4276  rabxp  4407  fconstmpt  4414  inxp  4497  cnvco  4547  rnmpt  4609  resundi  4652  resundir  4653  resindi  4654  resindir  4655  rescom  4663  resima  4670  imadmrn  4705  cnvimarndm  4716  cnvi  4755  rnun  4759  imaundi  4763  cnvxp  4769  imainrect  4793  imacnvcnv  4812  resdmres  4839  imadmres  4840  mptpreima  4841  cbviota  4899  sb8iota  4901  resdif  5175  cbvriota  5505  dfoprab2  5579  cbvoprab1  5603  cbvoprab2  5604  cbvoprab12  5605  cbvoprab3  5607  cbvmpt2x  5609  resoprab  5624  caov32  5715  caov31  5717  ofmres  5790  dfopab2  5842  dfxp3  5847  dmmpt2ssx  5852  fmpt2x  5853  tposco  5920  xpcomco  6330  dmaddpi  6480  dmmulpi  6481  dfplpq2  6509  dfmpq2  6510  dmaddpq  6534  dmmulpq  6535  axi2m1  7006  nummac  8470  decsubi  8488  9t11e99  8555  fzprval  9045  fztpval  9046  sqdivapi  9502  binom2i  9526  4bc2eq6  9641  shftidt2  9660  cji  9729
  Copyright terms: Public domain W3C validator