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  5618  isarep1  6441  findes  7611  axrepndlem1  10013  axrepndlem2  10014  nn0min  30536  esumcvg  31345  bj-sbidmOLD  34174  wl-nfs1t  34776  wl-sb6rft  34783  wl-equsb4  34792  wl-ax11-lem5  34820  sbcalf  35391  sbcexf  35392  opeliun2xp  44380