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  2696  cbvrexf  2697  cbvreu  2701  cbvralsv  2719  cbvrexsv  2720  cbvrab  2735  cbvreucsf  3121  cbvrabcsf  3122  sbss  3531  disjiun  3998  cbvopab1  4076  cbvmpt  4098  tfis  4582  findes  4602  cbviota  5183  sb8iota  5185  cbvriota  5840  uzind4s  9589  bezoutlemmain  11998  cbvrald  14510  setindft  14687