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 2050	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097

This theorem is referenced by:  sbelx  2289  sbequ12a  2290  sbid  2291  sbcov  2292  sbid2vw  2295  sb6rfv  2389  sbbib  2393  sb5rf  2499  sb6rf  2500  2sb5rf  2504  2sb6rf  2505  abbib  2832  opeliunxp  5728  opeliun2xp  5729  isarep1  6624  findes  7893  axrepndlem1  10572  axrepndlem2  10573  nn0min  33165  esumcvg  34476  bj-sbidmOLD  37485  bj-gabima  37576  bj-axseprep  37711  wl-nfs1t  38192  wl-sbid2ft  38200  wl-equsb4  38212  sbcalf  38763  sbcexf  38764