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

Theorem 3eqtr3rd 2179
 Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1
3eqtr3d.2
3eqtr3d.3
Assertion
Ref Expression
3eqtr3rd

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2
2 3eqtr3d.1 . . 3
3 3eqtr3d.2 . . 3
42, 3eqtr3d 2172 . 2
51, 4eqtr3d 2172 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1331 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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119 This theorem depends on definitions:  df-bi 116  df-cleq 2130 This theorem is referenced by:  fcofo  5678  fcof1o  5683  frecabcl  6289  nnaword  6400  enomnilem  7003  fodju0  7012  pn0sr  7572  negeu  7946  add20  8229  2halves  8942  bcnn  10496  bcpasc  10505  resqrexlemover  10775  fsumneg  11213  geolim  11273  geolim2  11274  mertensabs  11299  sincossq  11444  demoivre  11468  eirraplem  11472  gcdid  11663  gcdmultipled  11670  phiprmpw  11887  ioo2bl  12701  ptolemy  12894  coskpi  12918
 Copyright terms: Public domain W3C validator