Theorem sbequ12r 2294

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

Syntax hints:   → wi 4   ↔ wb 209  [wsb 2097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098

This theorem is referenced by:  sbelx  2295  sbequ12a  2296  sbid  2297  sbcov  2298  sbid2vw  2301  sb6rfv  2395  sbbib  2399  sb5rf  2505  sb6rf  2506  2sb5rf  2510  2sb6rf  2511  abbib  2838  opeliunxp  5726  opeliun2xp  5727  isarep1  6622  findes  7893  axrepndlem1  10573  axrepndlem2  10574  nn0min  33102  esumcvg  34417  bj-sbidmOLD  37370  bj-gabima  37460  bj-axseprep  37594  wl-nfs1t  38075  wl-sbid2ft  38083  wl-equsb4  38095  sbcalf  38648  sbcexf  38649