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

Theorem 3eqtr3ri 2219
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 2212 . 2  |-  B  =  C
51, 4eqtr3i 2212 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1364
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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182
This theorem is referenced by:  indif2  3394  resdm2  5137  co01  5161  cocnvres  5171  undifdc  6953  1mhlfehlf  9168  rei  10943  resqrexlemover  11054  cos1bnd  11802  6gcd4e2  12031  3lcm2e6  12195  cosq23lt0  14731  sincos4thpi  14738  sincos6thpi  14740  cosq34lt1  14748
  Copyright terms: Public domain W3C validator