Theorem sbequ12 1785

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 1782	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1783	. 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 1776

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 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524

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

This theorem is referenced by:  sbequ12r  1786  sbequ12a  1787  sbid  1788  ax16  1827  sb8h  1868  sb8eh  1869  sb8  1870  sb8e  1871  ax16ALT  1873  sbco  1987  sbcomxyyz  1991  sb9v  1997  sb6a  2007  mopick  2123  clelab  2322  sbab  2324  nfabdw  2358  cbvralf  2721  cbvrexf  2722  cbvralsv  2745  cbvrexsv  2746  cbvrab  2761  sbhypf  2813  mob2  2944  reu2  2952  reu6  2953  sbcralt  3066  sbcrext  3067  sbcralg  3068  sbcreug  3070  cbvreucsf  3149  cbvrabcsf  3150  cbvopab1  4106  cbvopab1s  4108  csbopabg  4111  cbvmptf  4127  cbvmpt  4128  opelopabsb  4294  frind  4387  tfis  4619  findes  4639  opeliunxp  4718  ralxpf  4812  rexxpf  4813  cbviota  5224  csbiotag  5251  cbvriota  5888  csbriotag  5890  abrexex2g  6177  opabex3d  6178  opabex3  6179  abrexex2  6181  dfoprab4f  6251  finexdc  6963  ssfirab  6997  uzind4s  9664  zsupcllemstep  10319  bezoutlemmain  12165  nnwosdc  12206  cbvrald  15434  bj-bdfindes  15595  bj-findes  15627