Theorem sbequ12r 2288

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  sbelx  2289  sbequ12a  2290  sbid  2291  sbcov  2292  sbid2vw  2294  sb6rfv  2387  sbbib  2391  sb5rf  2497  sb6rf  2498  2sb5rf  2502  2sb6rf  2503  abbib  2830  opeliunxp  5718  opeliun2xp  5719  isarep1  6626  findes  7910  axrepndlem1  10670  axrepndlem2  10671  nn0min  33405  esumcvg  34711  bj-sbidmOLD  37742  bj-gabima  37833  bj-axseprep  37970  wl-nfs1t  38449  wl-sbid2ft  38457  wl-equsb4  38469  sbcalf  39026  sbcexf  39027