Theorem sbequ12r 2291

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsb 2101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102

This theorem is used by:  sbelx  2292  sbequ12a  2293  sbid  2294  sbcov  2295  sbid2vw  2297  sb6rfv  2389  sbbib  2393  sb5rf  2499  sb6rf  2500  2sb5rf  2504  2sb6rf  2505  abbibOLD  2833  opeliunxp  5725  opeliun2xp  5726  isarep1  6658  findes  7946  axrepndlem1  10716  axrepndlem2  10717  nn0min  33508  esumcvg  34829  bj-sbidmOLD  37977  bj-gabima  38068  bj-axseprep  38260  wl-nfs1t  38737  wl-sbid2ft  38745  wl-equsb4  38757  sbcalf  39312  sbcexf  39313