Theorem sbequ12 1795

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 1792	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1793	. 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 1786

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 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534

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

This theorem is referenced by:  sbequ12r  1796  sbequ12a  1797  sbid  1798  ax16  1837  sb8h  1878  sb8eh  1879  sb8  1880  sb8e  1881  ax16ALT  1883  sbco  1997  sbcomxyyz  2001  sb9v  2007  sb6a  2017  mopick  2134  clelab  2333  sbab  2335  nfabdw  2369  cbvralf  2733  cbvrexf  2734  cbvralsv  2758  cbvrexsv  2759  cbvrab  2774  sbhypf  2827  mob2  2960  reu2  2968  reu6  2969  sbcralt  3082  sbcrext  3083  sbcralg  3084  sbcreug  3086  cbvreucsf  3166  cbvrabcsf  3167  cbvopab1  4133  cbvopab1s  4135  csbopabg  4138  cbvmptf  4154  cbvmpt  4155  opelopabsb  4324  frind  4417  tfis  4649  findes  4669  opeliunxp  4748  ralxpf  4842  rexxpf  4843  cbviota  5256  csbiotag  5283  cbvriota  5933  csbriotag  5935  abrexex2g  6228  opabex3d  6229  opabex3  6230  abrexex2  6232  dfoprab4f  6302  finexdc  7025  ssfirab  7059  uzind4s  9746  zsupcllemstep  10409  bezoutlemmain  12434  nnwosdc  12475  cbvrald  15924  bj-bdfindes  16084  bj-findes  16116