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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2170

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2062

This theorem is referenced by:  sbelx  2244  sbequ12a  2245  sbid  2246  sbid2vw  2249  sb6rfv  2351  sbbib  2355  sb5rf  2464  sb6rf  2465  2sb5rf  2469  2sb6rf  2470  abbib  2801  opeliunxp  5751  isarep1  6650  isarep1OLD  6651  findes  7918  axrepndlem1  10636  axrepndlem2  10637  nn0min  32769  esumcvg  33995  bj-sbidmOLD  36641  bj-gabima  36732  wl-nfs1t  37317  wl-sbid2ft  37325  wl-equsb4  37337  wl-ax11-lem5  37369  sbcalf  37900  sbcexf  37901  opeliun2xp  47833