Theorem sbequ12r 2286

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

Syntax hints:   → wi 4   ↔ wb 208  [wsb 2089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090

This theorem is referenced by:  sbelx  2287  sbequ12a  2288  sbid  2289  sbcov  2290  sbid2vw  2293  sb6rfv  2387  sbbib  2391  sb5rf  2497  sb6rf  2498  2sb5rf  2502  2sb6rf  2503  abbib  2830  opeliunxp  5710  opeliun2xp  5711  isarep1  6605  findes  7876  axrepndlem1  10544  axrepndlem2  10545  nn0min  32984  esumcvg  34344  bj-sbidmOLD  37296  bj-gabima  37386  bj-axseprep  37520  wl-nfs1t  38001  wl-sbid2ft  38009  wl-equsb4  38021  sbcalf  38574  sbcexf  38575