Theorem sbequ12r 2250

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066

This theorem is referenced by:  sbelx  2251  sbequ12a  2252  sbid  2253  sbid2vw  2256  sb6rfv  2372  sbbib  2376  sb5rf  2486  sb6rf  2487  2sb5rf  2492  2sb6rf  2493  abbi  2888  opeliunxp  5613  isarep1  6436  findes  7606  axrepndlem1  10008  axrepndlem2  10009  nn0min  30531  esumcvg  31340  bj-sbidmOLD  34169  wl-nfs1t  34771  wl-sb6rft  34778  wl-equsb4  34787  wl-ax11-lem5  34815  sbcalf  35386  sbcexf  35387  opeliun2xp  44375