Theorem sbequ 1761

Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sbequ	|- ( x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) )

Proof of Theorem sbequ

Step	Hyp	Ref	Expression
1		sbequi 1760	. 2 |- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
2		sbequi 1760	. . 3 |- ( y = x -> ( [ y / z ] ph -> [ x / z ] ph ) )
3	2	equcoms 1634	. 2 |- ( x = y -> ( [ y / z ] ph -> [ x / z ] ph ) )
4	1, 3	impbid 127	1 |- ( x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) )

Syntax hints:   -> wi 4   <-> wb 103   [wsb 1685

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686

This theorem is referenced by:  drsb2  1762  sbco2vlem  1861  sbco2yz  1878  sbcocom  1885  sb10f  1912  hbsb4  1929  nfsb4or  1940  sb8eu  1954  sb8euh  1964  cbvab  2201  cbvralf  2571  cbvrexf  2572  cbvreu  2575  cbvralsv  2588  cbvrexsv  2589  cbvrab  2599  cbvreucsf  2966  cbvrabcsf  2967  sbss  3349  cbvopab1  3851  cbvmpt  3872  tfis  4324  findes  4344  cbviota  4892  sb8iota  4894  cbvriota  5498  uzind4s  8678  bezoutlemmain  10387  cbvrald  10598  setindft  10760