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

Theorem 3eqtr4rd 2125
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
Hypotheses
Ref Expression
3eqtr4d.1  |-  ( ph  ->  A  =  B )
3eqtr4d.2  |-  ( ph  ->  C  =  A )
3eqtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr4rd
StepHypRef Expression
1 3eqtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
2 3eqtr4d.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2eqtr4d 2117 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2117 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  csbcnvg  4547  phplem4  6390  phplem4on  6402  recexnq  6642  prarloclemcalc  6754  addcomprg  6830  mulcomprg  6832  mulcmpblnrlemg  6979  axmulass  7101  divnegap  7861  modqlt  9415  modqmulnn  9424  iseqvalt  9532  iseqcaopr3  9556  ibcval5  9787  omgadd  9826  cjreb  9891  recj  9892  imcj  9900  imval2  9919  resqrexlemover  10034  sqrtmul  10059  amgm2  10142  maxabslemab  10230  flodddiv4  10478  dfgcd3  10543  absmulgcd  10550  sqpweven  10697  2sqpwodd  10698
  Copyright terms: Public domain W3C validator