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  4118  cbvopab1s  4120  csbopabg  4123  cbvmptf  4139  cbvmpt  4140  opelopabsb  4307  frind  4400  tfis  4632  findes  4652  opeliunxp  4731  ralxpf  4825  rexxpf  4826  cbviota  5238  csbiotag  5265  cbvriota  5912  csbriotag  5914  abrexex2g  6207  opabex3d  6208  opabex3  6209  abrexex2  6211  dfoprab4f  6281  finexdc  7001  ssfirab  7035  uzind4s  9713  zsupcllemstep  10374  bezoutlemmain  12352  nnwosdc  12393  cbvrald  15761  bj-bdfindes  15922  bj-findes  15954