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

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

Proof of Theorem equequ2
StepHypRef Expression
1 equtrr 1671 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
2 equtrr 1671 . . 3 (𝑦 = 𝑥 → (𝑧 = 𝑦𝑧 = 𝑥))
32equcoms 1669 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑦𝑧 = 𝑥))
41, 3impbid 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 1410  ax-ie2 1455  ax-8 1467  ax-17 1491  ax-i9 1495
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v2  1776  ax11v  1783  ax11ev  1784  equs5or  1786  eujust  1979  euf  1982  mo23  2018  eleq1w  2178  disjiun  3894  iotaval  5069  dffun4f  5109  dff13f  5639  supmoti  6848  isoti  6862  ennnfonelemr  11863  ctinf  11870
  Copyright terms: Public domain W3C validator