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

Theorem equequ1 1712
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 1504 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 1709 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 129 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  equveli  1759  drsb1  1799  equsb3lem  1950  euequ1  2121  axext3  2160  cbvreuvw  2709  reu6  2926  reu7  2932  disjiun  3998  cbviota  5183  dff13f  5770  poxp  6232  dcdifsnid  6504  supmoti  6991  isoti  7005  nninfwlpoim  7175  exmidontriimlem3  7221  exmidontriim  7223  netap  7252  fsum2dlemstep  11441  ennnfonelemr  12423  ctinf  12430  reap0  14776
  Copyright terms: Public domain W3C validator