Theorem sbequ12 1919

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 1918	. 2 |- (x = y -> (ph -> [y / x]ph))
2		sbequ2 1650	. 2 |- (x = y -> ([y / x]ph -> ph))
3	1, 2	impbid 183	1 |- (x = y -> (ph <-> [y / x]ph))

Syntax hints:   -> wi 4   <-> wb 176  [wsb 1648

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649

This theorem is referenced by:  sbequ12r  1920  sbequ12a  1921  sbid  1922  ax16ALT  2047  ax16ALT2  2048  nfsb4t  2080  sbco  2083  sbco2  2086  sbcom  2089  sbcom2  2114  sb6a  2116  sbal1  2126  mopick  2266  2mo  2282  2eu6  2289  clelab  2473  sbab  2475  cbvralf  2829  cbvralsv  2846  cbvrexsv  2847  cbvrab  2857  sbhypf  2904  mob2  3016  reu2  3024  reu6  3025  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  cbvreucsf  3200  cbvrabcsf  3201  csbifg  3690  cbviota  4344  csbiotag  4371  cbvopab1  4632  cbvopab1s  4634  csbopabg  4637  opelopabsb  4697  opeliunxp  4820  ralxpf  4827  cbvmpt  5676