ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqtr2d GIF version

Theorem eqtr2d 2118
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1 (𝜑𝐴 = 𝐵)
eqtr2d.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eqtr2d (𝜑𝐶 = 𝐴)

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 eqtr2d.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrd 2117 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2090 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  3eqtrrd  2122  3eqtr2rd  2124  ifandc  3413  onsucmin  4299  elxp4  4886  elxp5  4887  csbopeq1a  5917  ecinxp  6321  fundmen  6477  fidifsnen  6540  sbthlemi3  6615  addpinq1  6970  1idsr  7261  prsradd  7278  cnegexlem3  7606  cnegex  7607  submul2  7824  mulsubfacd  7843  divadddivap  8136  infrenegsupex  9017  fzval3  9546  fzoshftral  9580  ceiqm1l  9649  flqdiv  9659  flqmod  9676  intqfrac  9677  modqcyc2  9698  modqdi  9730  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  iseqid2  9847  expnegzap  9891  binom2sub  9968  binom3  9971  fihashssdif  10126  reim  10185  mulreap  10197  addcj  10224  resqrexlemcalc1  10346  absimle  10416  clim2iser  10622  serif0  10636  isummolem3  10664  divalglemnn  10824  dfgcd2  10909  lcmgcdlem  10965  lcm1  10969  oddpwdclemxy  11053  oddpwdclemdc  11057  hashgcdeq  11110
  Copyright terms: Public domain W3C validator