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

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

Proof of Theorem equequ2
StepHypRef Expression
1 equtrr 1669 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
2 equtrr 1669 . . 3 (𝑦 = 𝑥 → (𝑧 = 𝑦𝑧 = 𝑥))
32equcoms 1667 . 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 1408  ax-ie2 1453  ax-8 1465  ax-17 1489  ax-i9 1493 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  ax11v2  1774  ax11v  1781  ax11ev  1782  equs5or  1784  eujust  1977  euf  1980  mo23  2016  eleq1w  2176  disjiun  3892  iotaval  5067  dffun4f  5107  dff13f  5637  supmoti  6846  isoti  6860  ennnfonelemr  11842  ctinf  11849
 Copyright terms: Public domain W3C validator