Theorem sbequ12 1771

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 1768	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1769	. 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 1762

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 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510

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

This theorem is referenced by:  sbequ12r  1772  sbequ12a  1773  sbid  1774  ax16  1813  sb8h  1854  sb8eh  1855  sb8  1856  sb8e  1857  ax16ALT  1859  sbco  1968  sbcomxyyz  1972  sb9v  1978  sb6a  1988  mopick  2104  clelab  2303  sbab  2305  nfabdw  2338  cbvralf  2696  cbvrexf  2697  cbvralsv  2719  cbvrexsv  2720  cbvrab  2735  sbhypf  2786  mob2  2917  reu2  2925  reu6  2926  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcreug  3043  cbvreucsf  3121  cbvrabcsf  3122  cbvopab1  4076  cbvopab1s  4078  csbopabg  4081  cbvmptf  4097  cbvmpt  4098  opelopabsb  4260  frind  4352  tfis  4582  findes  4602  opeliunxp  4681  ralxpf  4773  rexxpf  4774  cbviota  5183  csbiotag  5209  cbvriota  5840  csbriotag  5842  abrexex2g  6120  opabex3d  6121  opabex3  6122  abrexex2  6124  dfoprab4f  6193  finexdc  6901  ssfirab  6932  uzind4s  9588  zsupcllemstep  11940  bezoutlemmain  11993  nnwosdc  12034  cbvrald  14422  bj-bdfindes  14583  bj-findes  14615