Theorem sbequ12 1701

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

Syntax hints:   -> wi 4   <-> wb 103   [wsb 1692

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445

This theorem depends on definitions:  df-bi 115  df-sb 1693

This theorem is referenced by:  sbequ12r  1702  sbequ12a  1703  sbid  1704  ax16  1741  sb8h  1782  sb8eh  1783  sb8  1784  sb8e  1785  ax16ALT  1787  sbco  1890  sbcomxyyz  1894  sb9v  1902  sb6a  1912  mopick  2026  clelab  2212  sbab  2214  cbvralf  2584  cbvrexf  2585  cbvralsv  2601  cbvrexsv  2602  cbvrab  2617  sbhypf  2668  mob2  2795  reu2  2803  reu6  2804  sbcralt  2915  sbcrext  2916  sbcralg  2917  sbcreug  2919  cbvreucsf  2992  cbvrabcsf  2993  cbvopab1  3911  cbvopab1s  3913  csbopabg  3916  cbvmptf  3932  cbvmpt  3933  opelopabsb  4087  frind  4179  tfis  4398  findes  4418  opeliunxp  4493  ralxpf  4582  rexxpf  4583  cbviota  4985  csbiotag  5008  cbvriota  5618  csbriotag  5620  abrexex2g  5891  opabex3d  5892  opabex3  5893  abrexex2  5895  dfoprab4f  5963  finexdc  6616  ssfirab  6641  uzind4s  9076  zsupcllemstep  11215  bezoutlemmain  11261  cbvrald  11643  bj-bdfindes  11799  bj-findes  11831