Theorem sbequ12 1820

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 1817	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1818	. 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 1811

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 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

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

This theorem is referenced by:  sbequ12r  1821  sbequ12a  1822  sbid  1823  ax16  1862  sb8h  1903  sb8eh  1904  sb8  1905  sb8e  1906  ax16ALT  1908  sbco  2024  sbcomxyyz  2028  sb9v  2034  sb6a  2044  mopick  2161  clelab  2362  sbab  2364  nfabdw  2405  cbvralf  2771  cbvrexf  2772  cbvralsv  2796  cbvrexsv  2797  cbvrab  2813  sbhypf  2866  mob2  2999  reu2  3007  reu6  3008  sbcralt  3121  sbcrext  3122  sbcralg  3123  sbcreug  3125  cbvreucsf  3205  cbvrabcsf  3206  cbvopab1  4185  cbvopab1s  4187  csbopabg  4190  cbvmptf  4206  cbvmpt  4207  opelopabsb  4380  frind  4475  tfis  4707  findes  4727  opeliunxp  4807  ralxpf  4903  rexxpf  4904  cbviota  5319  csbiotag  5347  cbvriota  6017  csbriotag  6019  abrexex2g  6315  opabex3d  6316  opabex3  6317  abrexex2  6319  dfoprab4f  6389  modom  7063  finexdc  7162  ssfirab  7199  uzind4s  9925  zsupcllemstep  10593  bezoutlemmain  12698  nnwosdc  12739  cbvrald  16577  bj-bdfindes  16736  bj-findes  16768