Theorem sbequ12r 2243

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

Syntax hints:   → wi 4   ↔ wb 205  [wsb 2066

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 1912  ax-6 1970  ax-7 2010  ax-12 2170

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067

This theorem is referenced by:  sbelx  2244  sbequ12a  2245  sbid  2246  sbid2vw  2249  sb6rfv  2352  sbbib  2356  sb5rf  2465  sb6rf  2466  2sb5rf  2470  2sb6rf  2471  abbib  2803  opeliunxp  5743  isarep1  6637  isarep1OLD  6638  findes  7897  axrepndlem1  10591  axrepndlem2  10592  nn0min  32294  esumcvg  33383  bj-sbidmOLD  36033  bj-gabima  36124  wl-nfs1t  36710  wl-sb6rft  36717  wl-equsb4  36726  wl-ax11-lem5  36755  sbcalf  37286  sbcexf  37287  opeliun2xp  47097