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

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

Proof of Theorem syl6req
StepHypRef Expression
1 syl6req.1 . . 3 (𝜑𝐴 = 𝐵)
2 syl6req.2 . . 3 𝐵 = 𝐶
31, 2syl6eq 2188 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2145 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 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  syl6reqr  2191  elxp4  5026  elxp5  5027  fo1stresm  6059  fo2ndresm  6060  eloprabi  6094  fo2ndf  6124  xpsnen  6715  xpassen  6724  ac6sfi  6792  undifdc  6812  ine0  8168  nn0n0n1ge2  9133  fzval2  9805  fseq1p1m1  9886  fsum2dlemstep  11215  modfsummodlemstep  11238  ef4p  11412  sin01bnd  11475  odd2np1  11581  sqpweven  11864  2sqpwodd  11865  psmetdmdm  12507  xmetdmdm  12539  dveflem  12870  reeff1oleme  12876  abssinper  12949
 Copyright terms: Public domain W3C validator