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

Theorem sbequ12r 1998
Description: An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sbequ12r  |-  ( x  =  y  ->  ( [ x  /  y ] ph  <->  ph ) )

Proof of Theorem sbequ12r
StepHypRef Expression
1 sbequ12 1997 . . 3  |-  ( y  =  x  ->  ( ph 
<->  [ x  /  y ] ph ) )
21bicomd 201 . 2  |-  ( y  =  x  ->  ( [ x  /  y ] ph  <->  ph ) )
32equcoms 1800 1  |-  ( x  =  y  ->  ( [ x  /  y ] ph  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [wsb 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-sb 1745
This theorem is referenced by:  sbequ12a  1999  sbid  2001  sbidmOLD  2159  sb5rf  2167  sb6rf  2168  2sb5rf  2197  2sb6rf  2198  abbiOLD  2586  opeliunxp  5040  isarep1  5649  findes  6703  axrepndlem1  8958  axrepndlem2  8959  nn0min  27845  esumcvg  28315  wl-nfs1t  30231  wl-sb6rft  30237  wl-equsb4  30245  wl-ax11-lem5  30269  sbcalf  30757  sbcexf  30758  opeliun2xp  33176  bj-abbi  34762
  Copyright terms: Public domain W3C validator