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 2052	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099

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  5717  opeliun2xp  5718  isarep1  6631  findes  7914  axrepndlem1  10682  axrepndlem2  10683  nn0min  33460  esumcvg  34766  bj-sbidmOLD  37856  bj-gabima  37947  bj-axseprep  38096  wl-nfs1t  38576  wl-sbid2ft  38584  wl-equsb4  38596  sbcalf  39153  sbcexf  39154