Theorem sbequ12 1794

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

Syntax hints:   -> wi 4   <-> wb 105   [wsb 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533

This theorem depends on definitions:  df-bi 117  df-sb 1786

This theorem is referenced by:  sbequ12r  1795  sbequ12a  1796  sbid  1797  ax16  1836  sb8h  1877  sb8eh  1878  sb8  1879  sb8e  1880  ax16ALT  1882  sbco  1996  sbcomxyyz  2000  sb9v  2006  sb6a  2016  mopick  2132  clelab  2331  sbab  2333  nfabdw  2367  cbvralf  2730  cbvrexf  2731  cbvralsv  2754  cbvrexsv  2755  cbvrab  2770  sbhypf  2822  mob2  2953  reu2  2961  reu6  2962  sbcralt  3075  sbcrext  3076  sbcralg  3077  sbcreug  3079  cbvreucsf  3158  cbvrabcsf  3159  cbvopab1  4117  cbvopab1s  4119  csbopabg  4122  cbvmptf  4138  cbvmpt  4139  opelopabsb  4306  frind  4399  tfis  4631  findes  4651  opeliunxp  4730  ralxpf  4824  rexxpf  4825  cbviota  5237  csbiotag  5264  cbvriota  5910  csbriotag  5912  abrexex2g  6205  opabex3d  6206  opabex3  6207  abrexex2  6209  dfoprab4f  6279  finexdc  6999  ssfirab  7033  uzind4s  9711  zsupcllemstep  10372  bezoutlemmain  12319  nnwosdc  12360  cbvrald  15724  bj-bdfindes  15885  bj-findes  15917