Theorem sbequ12 1651

Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sbequ12	|- (x = y -> (ph <-> [y / x]ph))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 1648	. 2 |- (x = y -> (ph -> [y / x]ph))
2		sbequ2 1649	. 2 |- (x = y -> ([y / x]ph -> ph))
3	1, 2	impbid 120	1 |- (x = y -> (ph <-> [y / x]ph))

Syntax hints:   -> wi 4   <-> wb 98  [wsb 1642

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397

This theorem depends on definitions:  df-bi 110  df-sb 1643

This theorem is referenced by:  sbequ12r  1652  sbequ12a  1653  sbid  1654  ax16  1691  sb8h  1731  sb8eh  1732  sb8  1733  sb8e  1734  ax16ALT  1736  sbco  1839  sbcomxyyz  1843  sb9v  1851  sb6a  1861  mopick  1975  clelab  2159  sbab  2161  cbvralf  2521  cbvrexf  2522  cbvralsv  2538  cbvrexsv  2539  cbvrab  2549  sbhypf  2597  mob2  2715  reu2  2723  reu6  2724  sbcralt  2828  sbcrext  2829  sbcralg  2830  sbcrexg  2831  sbcreug  2832  cbvreucsf  2904  cbvrabcsf  2905  cbvopab1  3821  cbvopab1s  3823  csbopabg  3826  cbvmpt  3842  opelopabsb  3988  tfis  4249  findes  4269  opeliunxp  4338  ralxpf  4425  rexxpf  4426  cbviota  4815  csbiotag  4838  cbvriota  5421  csbriotag  5423  abrexex2g  5689  opabex3d  5690  opabex3  5691  abrexex2  5693  dfoprab4f  5761  uzind4s  8309  cbvrald  9262  bj-bdfindes  9409  bj-findes  9441