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

Theorem 3eqtr4i 2048
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
3eqtr4i.2  C
3eqtr4i.3  D
Assertion
Ref Expression
3eqtr4i  C  D

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2  C
2 3eqtr4i.3 . . 3  D
3 3eqtr4i.1 . . 3
42, 3eqtr4i 2041 . 2  D
51, 4eqtr4i 2041 1  C  D
Colors of variables: wff set class
Syntax hints:   wceq 1226
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 1312  ax-gen 1314  ax-4 1377  ax-17 1396  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011
This theorem is referenced by:  rabswap  2462  rabbiia  2521  cbvrab  2529  cbvcsb  2829  csbco  2834  cbvrabcsf  2884  un4  3076  in13  3123  in31  3124  in4  3126  indifcom  3156  indir  3159  undir  3160  notrab  3187  dfnul3  3200  rab0  3219  prcom  3416  tprot  3433  tpcoma  3434  tpcomb  3435  tpass  3436  qdassr  3438  pw0  3481  opid  3537  int0  3599  cbviun  3664  cbviin  3665  iunrab  3674  iunin1  3691  cbvopab  3798  cbvopab1  3800  cbvopab2  3801  cbvopab1s  3802  cbvopab2v  3804  unopab  3806  cbvmpt  3821  iunopab  3988  uniuni  4129  onsucelsucexmidlem  4194  rabxp  4303  fconstmpt  4310  inxp  4393  cnvco  4443  rnmpt  4505  resundi  4548  resundir  4549  resindi  4550  resindir  4551  rescom  4559  resima  4566  imadmrn  4601  cnvimarndm  4612  cnvi  4651  rnun  4655  imaundi  4659  cnvxp  4665  imainrect  4689  imacnvcnv  4708  resdmres  4735  imadmres  4736  mptpreima  4737  cbviota  4795  sb8iota  4797  resdif  5069  cbvriota  5398  dfoprab2  5471  cbvoprab1  5495  cbvoprab2  5496  cbvoprab12  5497  cbvoprab3  5499  cbvmpt2x  5501  resoprab  5516  caov32  5607  caov31  5609  ofmres  5682  dfopab2  5734  dfxp3  5739  dmmpt2ssx  5744  fmpt2x  5745  tposco  5808  dmaddpi  6179  dmmulpi  6180  dfplpq2  6207  dfmpq2  6208  dmaddpq  6232  dmmulpq  6233  axi2m1  6568
  Copyright terms: Public domain W3C validator