Theorem sbequ12 1744

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

Syntax hints:   -> wi 4   <-> wb 104   [wsb 1735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487

This theorem depends on definitions:  df-bi 116  df-sb 1736

This theorem is referenced by:  sbequ12r  1745  sbequ12a  1746  sbid  1747  ax16  1785  sb8h  1826  sb8eh  1827  sb8  1828  sb8e  1829  ax16ALT  1831  sbco  1941  sbcomxyyz  1945  sb9v  1953  sb6a  1963  mopick  2077  clelab  2265  sbab  2267  cbvralf  2648  cbvrexf  2649  cbvralsv  2668  cbvrexsv  2669  cbvrab  2684  sbhypf  2735  mob2  2864  reu2  2872  reu6  2873  sbcralt  2985  sbcrext  2986  sbcralg  2987  sbcreug  2989  cbvreucsf  3064  cbvrabcsf  3065  cbvopab1  4001  cbvopab1s  4003  csbopabg  4006  cbvmptf  4022  cbvmpt  4023  opelopabsb  4182  frind  4274  tfis  4497  findes  4517  opeliunxp  4594  ralxpf  4685  rexxpf  4686  cbviota  5093  csbiotag  5116  cbvriota  5740  csbriotag  5742  abrexex2g  6018  opabex3d  6019  opabex3  6020  abrexex2  6022  dfoprab4f  6091  finexdc  6796  ssfirab  6822  uzind4s  9385  zsupcllemstep  11638  bezoutlemmain  11686  cbvrald  12995  bj-bdfindes  13147  bj-findes  13179