MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equequ1 Structured version   Unicode version

Theorem equequ1 1747
Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
Assertion
Ref Expression
equequ1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )

Proof of Theorem equequ1
StepHypRef Expression
1 ax-7 1739 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1745 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 191 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  equequ2  1748  drsb1  2091  equsb3lem  2158  dveeq1-o  2258  dveeq1-o16  2259  axc11n-16  2261  ax12eq  2264  sb8eu  2314  2moOLDOLD  2384  2eu6OLD  2394  euequ1OLD  2397  axext3OLD  2448  reu6  3297  reu7  3303  disjxun  4451  cbviota  5562  dff13f  6166  poxp  6907  unxpdomlem1  7736  unxpdomlem2  7737  aceq0  8511  zfac  8852  axrepndlem1  8979  axpowndlem2OLD  8986  zfcndac  9009  injresinj  11906  fsum2dlem  13565  ramub1lem2  14421  ramcl  14423  symgextf1  16318  mamulid  18812  mamurid  18813  mdetdiagid  18971  mdetunilem9  18991  alexsubALTlem3  20417  ptcmplem2  20421  dscmet  20961  dyadmbllem  21876  opnmbllem  21878  isppw2  23255  frg2wot1  24881  disji2f  27261  disjif2  27265  ghomf1olem  28859  wl-equsb3  29931  bfp  30247  fphpd  30678  lcoss  32519  ax6e2nd  32812  ax6e2ndVD  33189  ax6e2ndALT  33211  bj-axext3  33836
  Copyright terms: Public domain W3C validator