Theorem sbequ12r 2245

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

Syntax hints:   → wi 4   ↔ wb 205  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068

This theorem is referenced by:  sbelx  2246  sbequ12a  2247  sbid  2248  sbid2vw  2251  sb6rfv  2355  sbbib  2359  sb5rf  2467  sb6rf  2468  2sb5rf  2472  2sb6rf  2473  abbi  2810  opeliunxp  5654  isarep1  6522  findes  7749  axrepndlem1  10348  axrepndlem2  10349  nn0min  31134  esumcvg  32054  bj-sbidmOLD  35034  bj-gabima  35128  wl-nfs1t  35696  wl-sb6rft  35703  wl-equsb4  35712  wl-ax11-lem5  35740  sbcalf  36272  sbcexf  36273  opeliun2xp  45668