Theorem sbequ 1840

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 1839	. 2 |- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
2		sbequi 1839	. . 3 |- ( y = x -> ( [ y / z ] ph -> [ x / z ] ph ) )
3	2	equcoms 1708	. 2 |- ( x = y -> ( [ y / z ] ph -> [ x / z ] ph ) )
4	1, 3	impbid 129	1 |- ( x = y -> ( [ x / z ] ph <-> [ y / z ] 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-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535

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

This theorem is referenced by:  drsb2  1841  sbco2vlem  1944  sbco2v  1948  sbco2yz  1963  sbcocom  1970  sb10f  1995  hbsb4  2012  nfsb4or  2021  sb8eu  2039  sb8euh  2049  cbvab  2301  cbvralf  2697  cbvrexf  2698  cbvreu  2703  cbvralsv  2721  cbvrexsv  2722  cbvrab  2737  cbvreucsf  3123  cbvrabcsf  3124  sbss  3533  disjiun  4000  cbvopab1  4078  cbvmpt  4100  tfis  4584  findes  4604  cbviota  5185  sb8iota  5187  cbvriota  5843  uzind4s  9592  bezoutlemmain  12001  cbvrald  14579  setindft  14756