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

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2062

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 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063

This theorem is referenced by:  sbelx  2251  sbequ12a  2252  sbid  2253  sbcov  2254  sbid2vw  2257  sb6rfv  2358  sbbib  2362  sb5rf  2470  sb6rf  2471  2sb5rf  2475  2sb6rf  2476  abbib  2809  opeliunxp  5756  isarep1  6657  isarep1OLD  6658  findes  7923  axrepndlem1  10630  axrepndlem2  10631  nn0min  32827  esumcvg  34067  bj-sbidmOLD  36833  bj-gabima  36923  wl-nfs1t  37518  wl-sbid2ft  37526  wl-equsb4  37538  wl-ax11-lem5  37570  sbcalf  38101  sbcexf  38102  opeliun2xp  48178