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

Theorem 3eqtr3ri 2207
Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
Hypotheses
Ref Expression
3eqtr3i.1  |-  A  =  B
3eqtr3i.2  |-  A  =  C
3eqtr3i.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3ri  |-  D  =  C

Proof of Theorem 3eqtr3ri
StepHypRef Expression
1 3eqtr3i.3 . 2  |-  B  =  D
2 3eqtr3i.1 . . 3  |-  A  =  B
3 3eqtr3i.2 . . 3  |-  A  =  C
42, 3eqtr3i 2200 . 2  |-  B  =  C
51, 4eqtr3i 2200 1  |-  D  =  C
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:  indif2  3379  resdm2  5119  co01  5143  cocnvres  5153  undifdc  6922  1mhlfehlf  9136  rei  10907  resqrexlemover  11018  cos1bnd  11766  6gcd4e2  11995  3lcm2e6  12159  cosq23lt0  14224  sincos4thpi  14231  sincos6thpi  14233  cosq34lt1  14241
  Copyright terms: Public domain W3C validator