Theorem sbequ12r 2250

Description: An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
sbequ12r	⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))

Proof of Theorem sbequ12r

Step	Hyp	Ref	Expression
1		sbequ12 2249	. . 3 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ [𝑥 / 𝑦]𝜑))
2	1	bicomd 226	. 2 ⊢ (𝑦 = 𝑥 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))
3	2	equcoms 2028	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209  [wsb 2070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071

This theorem is referenced by:  sbelx  2251  sbequ12a  2252  sbid  2253  sbid2vw  2256  sb6rfv  2356  sbbib  2360  sb5rf  2466  sb6rf  2467  2sb5rf  2471  2sb6rf  2472  abbi  2810  opeliunxp  5616  isarep1  6468  findes  7680  axrepndlem1  10206  axrepndlem2  10207  nn0min  30854  esumcvg  31766  bj-sbidmOLD  34771  bj-gabima  34865  wl-nfs1t  35433  wl-sb6rft  35440  wl-equsb4  35449  wl-ax11-lem5  35477  sbcalf  36009  sbcexf  36010  opeliun2xp  45341