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

Theorem equequ1 1692
 Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
equequ1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))

Proof of Theorem equequ1
StepHypRef Expression
1 ax-8 1484 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 1689 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 128 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 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-gen 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  equveli  1739  drsb1  1779  equsb3lem  1930  euequ1  2101  axext3  2140  cbvreuvw  2686  reu6  2901  reu7  2907  disjiun  3960  cbviota  5137  dff13f  5715  poxp  6173  dcdifsnid  6444  supmoti  6929  isoti  6943  exmidontriimlem3  7141  exmidontriim  7143  fsum2dlemstep  11313  ennnfonelemr  12124  ctinf  12131  reap0  13591
 Copyright terms: Public domain W3C validator