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

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

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3  |-  A  =  B
2 3eqtr3i.2 . . 3  |-  A  =  C
31, 2eqtr3i 2200 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2200 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  csbvarg  3087  un12  3295  in12  3348  indif1  3382  difundir  3390  difindir  3392  dif32  3400  resmpt3  4958  xp0  5050  fvsnun1  5716  caov12  6066  caov13  6068  djuassen  7219  xpdjuen  7220  rec1nq  7397  halfnqq  7412  negsubdii  8245  halfpm6th  9142  decmul1  9450  i4  10626  fac4  10716  imi  10912  resqrexlemover  11022  ef01bndlem  11767  znnen  12402  sn0cld  13798  cospi  14382  sincos4thpi  14422  sincos3rdpi  14425  lgsdir2lem1  14590  lgsdir2lem5  14594  2lgsoddprmlem3d  14619  ex-bc  14642  ex-gcd  14644
  Copyright terms: Public domain W3C validator