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

Theorem 3eqtr3ri 2147
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 2140 . 2  |-  B  =  C
51, 4eqtr3i 2140 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  indif2  3290  resdm2  4999  co01  5023  cocnvres  5033  undifdc  6780  1mhlfehlf  8906  rei  10639  resqrexlemover  10750  cos1bnd  11393  6gcd4e2  11610  3lcm2e6  11765  cosq23lt0  12841  sincos4thpi  12848  sincos6thpi  12850  cosq34lt1  12858
  Copyright terms: Public domain W3C validator