Theorem sbequ12r 2290

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 2289	. . 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 2216

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

This theorem is used by:  sbelx  2291  sbequ12a  2292  sbid  2293  sbcov  2294  sbid2vw  2297  sb6rfv  2391  sbbib  2395  sb5rf  2501  sb6rf  2502  2sb5rf  2506  2sb6rf  2507  abbib  2834  opeliunxp  5730  opeliun2xp  5731  isarep1  6628  findes  7899  axrepndlem1  10588  axrepndlem2  10589  nn0min  33211  esumcvg  34516  bj-sbidmOLD  37518  bj-gabima  37609  bj-axseprep  37744  wl-nfs1t  38225  wl-sbid2ft  38233  wl-equsb4  38245  sbcalf  38796  sbcexf  38797