Theorem sbequ12 1751

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 1748	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1749	. 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 1742

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 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490

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

This theorem is referenced by:  sbequ12r  1752  sbequ12a  1753  sbid  1754  ax16  1793  sb8h  1834  sb8eh  1835  sb8  1836  sb8e  1837  ax16ALT  1839  sbco  1948  sbcomxyyz  1952  sb9v  1958  sb6a  1968  mopick  2084  clelab  2283  sbab  2285  nfabdw  2318  cbvralf  2674  cbvrexf  2675  cbvralsv  2694  cbvrexsv  2695  cbvrab  2710  sbhypf  2761  mob2  2892  reu2  2900  reu6  2901  sbcralt  3013  sbcrext  3014  sbcralg  3015  sbcreug  3017  cbvreucsf  3095  cbvrabcsf  3096  cbvopab1  4037  cbvopab1s  4039  csbopabg  4042  cbvmptf  4058  cbvmpt  4059  opelopabsb  4220  frind  4312  tfis  4541  findes  4561  opeliunxp  4640  ralxpf  4731  rexxpf  4732  cbviota  5139  csbiotag  5162  cbvriota  5787  csbriotag  5789  abrexex2g  6065  opabex3d  6066  opabex3  6067  abrexex2  6069  dfoprab4f  6138  finexdc  6844  ssfirab  6875  uzind4s  9495  zsupcllemstep  11824  bezoutlemmain  11873  cbvrald  13333  bj-bdfindes  13495  bj-findes  13527