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

Theorem sbequ12r 1962
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 1961 . . 3  |-  ( y  =  x  ->  ( ph 
<->  [ x  /  y ] ph ) )
21bicomd 201 . 2  |-  ( y  =  x  ->  ( [ x  /  y ] ph  <->  ph ) )
32equcoms 1744 1  |-  ( x  =  y  ->  ( [ x  /  y ] ph  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [wsb 1711
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  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-sb 1712
This theorem is referenced by:  sbequ12a  1963  sbid  1965  sbidmOLD  2133  sb5rf  2143  sb6rf  2145  2sb5rf  2181  2sb6rf  2182  abbiOLD  2599  opeliunxp  5050  isarep1  5665  findes  6708  axrepndlem1  8963  axrepndlem2  8964  nn0min  27279  esumcvg  27732  wl-nfs1t  29568  wl-sb6rft  29574  wl-equsb4  29582  wl-ax11-lem5  29606  sbcalf  30120  sbcexf  30121  opeliun2xp  31986  bj-abbi  33442
  Copyright terms: Public domain W3C validator