Theorem sbequ12 1654

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

Syntax hints:   -> wi 4   <-> wb 98   [wsb 1645

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400

This theorem depends on definitions:  df-bi 110  df-sb 1646

This theorem is referenced by:  sbequ12r  1655  sbequ12a  1656  sbid  1657  ax16  1694  sb8h  1734  sb8eh  1735  sb8  1736  sb8e  1737  ax16ALT  1739  sbco  1842  sbcomxyyz  1846  sb9v  1854  sb6a  1864  mopick  1978  clelab  2162  sbab  2164  cbvralf  2527  cbvrexf  2528  cbvralsv  2544  cbvrexsv  2545  cbvrab  2555  sbhypf  2603  mob2  2721  reu2  2729  reu6  2730  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  cbvreucsf  2910  cbvrabcsf  2911  cbvopab1  3830  cbvopab1s  3832  csbopabg  3835  cbvmpt  3851  opelopabsb  3997  frind  4089  tfis  4306  findes  4326  opeliunxp  4395  ralxpf  4482  rexxpf  4483  cbviota  4872  csbiotag  4895  cbvriota  5478  csbriotag  5480  abrexex2g  5747  opabex3d  5748  opabex3  5749  abrexex2  5751  dfoprab4f  5819  uzind4s  8533  cbvrald  9927  bj-bdfindes  10074  bj-findes  10106