Theorem sbequ12r 2242

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066

This theorem is referenced by:  sbelx  2243  sbequ12a  2244  sbid  2245  sbid2vw  2248  sb6rfv  2351  sbbib  2355  sb5rf  2464  sb6rf  2465  2sb5rf  2469  2sb6rf  2470  abbib  2802  opeliunxp  5742  isarep1  6636  isarep1OLD  6637  findes  7895  axrepndlem1  10589  axrepndlem2  10590  nn0min  32293  esumcvg  33382  bj-sbidmOLD  36032  bj-gabima  36123  wl-nfs1t  36709  wl-sb6rft  36716  wl-equsb4  36725  wl-ax11-lem5  36754  sbcalf  37285  sbcexf  37286  opeliun2xp  47096