Theorem sbequ12r 2219

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 2218	. . 3 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ [𝑥 / 𝑦]𝜑))
2	1	bicomd 224	. 2 ⊢ (𝑦 = 𝑥 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))
3	2	equcoms 2008	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 207  [wsb 2044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-12 2143

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-sb 2045

This theorem is referenced by:  sbelx  2220  sbequ12a  2221  sbid  2222  sb6rfv  2335  sbbib  2339  sb5rf  2449  sb6rf  2450  2sb5rf  2455  2sb6rf  2456  2sb6rfOLD  2457  opeliunxp  5512  isarep1  6319  findes  7475  axrepndlem1  9867  axrepndlem2  9868  nn0min  30217  esumcvg  30958  bj-abbi  33698  bj-sbidmOLD  33750  wl-nfs1t  34330  wl-sb6rft  34337  wl-equsb4  34345  wl-ax11-lem5  34373  sbcalf  34945  sbcexf  34946  opeliun2xp  43881