Theorem sbequ12r 2264

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

Syntax hints:   → wi 4   ↔ wb 207  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074

This theorem is referenced by:  sbelx  2265  sbequ12a  2266  sbid  2267  sbcov  2268  sbid2vw  2271  sb6rfv  2365  sbbib  2369  sb5rf  2475  sb6rf  2476  2sb5rf  2480  2sb6rf  2481  abbib  2808  opeliunxp  5685  opeliun2xp  5686  isarep1  6574  findes  7840  axrepndlem1  10506  axrepndlem2  10507  nn0min  32913  esumcvg  34270  bj-sbidmOLD  37203  bj-gabima  37293  bj-axseprep  37427  wl-nfs1t  37908  wl-sbid2ft  37916  wl-equsb4  37928  sbcalf  38481  sbcexf  38482