Theorem sbequ12r 2257

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

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068

This theorem is referenced by:  sbelx  2258  sbequ12a  2259  sbid  2260  sbcov  2261  sbid2vw  2264  sb6rfv  2359  sbbib  2363  sb5rf  2469  sb6rf  2470  2sb5rf  2474  2sb6rf  2475  abbib  2802  opeliunxp  5688  opeliun2xp  5689  isarep1  6578  findes  7839  axrepndlem1  10494  axrepndlem2  10495  nn0min  32829  esumcvg  34171  bj-sbidmOLD  36967  bj-gabima  37057  wl-nfs1t  37654  wl-sbid2ft  37662  wl-equsb4  37674  sbcalf  38227  sbcexf  38228