Theorem sbequ12r 2287

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

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

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 1943  ax-6 2000  ax-7 2041  ax-12 2213

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

This theorem is used by:  sbelx  2288  sbequ12a  2289  sbid  2290  sbcov  2291  sbid2vw  2293  sb6rfv  2386  sbbib  2390  sb5rf  2496  sb6rf  2497  2sb5rf  2501  2sb6rf  2502  abbib  2829  opeliunxp  5722  opeliun2xp  5723  isarep1  6621  findes  7897  axrepndlem1  10601  axrepndlem2  10602  nn0min  33291  esumcvg  34596  bj-sbidmOLD  37593  bj-gabima  37684  bj-axseprep  37819  wl-nfs1t  38300  wl-sbid2ft  38308  wl-equsb4  38320  sbcalf  38862  sbcexf  38863