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

Theorem eqtr4id 2192
 Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
eqtr4id.2 𝐴 = 𝐵
eqtr4id.1 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
eqtr4id (𝜑𝐴 = 𝐶)

Proof of Theorem eqtr4id
StepHypRef Expression
1 eqtr4id.1 . 2 (𝜑𝐶 = 𝐵)
2 eqtr4id.2 . . 3 𝐴 = 𝐵
32eqcomi 2144 . 2 𝐵 = 𝐴
41, 3eqtr2di 2190 1 (𝜑𝐴 = 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  iftrue  3485  iffalse  3488  difprsn1  3668  dmmptg  5047  relcoi1  5081  funimacnv  5210  dmmptd  5264  dffv3g  5428  dfimafn  5481  fvco2  5501  isoini  5730  oprabco  6125  ixpconstg  6612  unfiexmid  6822  undifdc  6828  sbthlemi4  6864  sbthlemi5  6865  sbthlemi6  6866  supval2ti  6898  exmidfodomrlemim  7084  suplocexprlemex  7581  eqneg  8543  zeo  9207  fseq1p1m1  9932  seq3val  10289  seqvalcd  10290  hashfzo  10627  hashxp  10631  fsumconst  11282  modfsummod  11286  telfsumo  11294  mulgcd  11774  algcvg  11799  phiprmpw  11968  strslfv3  12077  uptx  12516  resubmet  12790
 Copyright terms: Public domain W3C validator