Theorem sbequ12 1632

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 1629	. 2 |- (x = y -> (ph -> [y / x]ph))
2		sbequ2 1630	. 2 |- (x = y -> ([y / x]ph -> ph))
3	1, 2	impbid 120	1 |- (x = y -> (ph <-> [y / x]ph))

Syntax hints:   -> wi 4   <-> wb 98  [wsb 1623

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377

This theorem depends on definitions:  df-bi 110  df-sb 1624

This theorem is referenced by:  sbequ12r  1633  sbequ12a  1634  sbid  1635  ax16  1672  sb8h  1712  sb8eh  1713  sb8  1714  sb8e  1715  ax16ALT  1717  sbco  1820  sbcomxyyz  1824  sb9v  1832  sb6a  1842  mopick  1956  clelab  2140  sbab  2142  cbvralf  2501  cbvrexf  2502  cbvralsv  2518  cbvrexsv  2519  cbvrab  2529  sbhypf  2576  mob2  2694  reu2  2702  reu6  2703  sbcralt  2807  sbcrext  2808  sbcralg  2809  sbcrexg  2810  sbcreug  2811  cbvreucsf  2883  cbvrabcsf  2884  cbvopab1  3800  cbvopab1s  3802  csbopabg  3805  cbvmpt  3821  opelopabsb  3967  tfis  4229  findes  4249  opeliunxp  4318  ralxpf  4405  rexxpf  4406  cbviota  4795  csbiotag  4818  cbvriota  5398  csbriotag  5400  abrexex2g  5666  opabex3d  5667  opabex3  5668  abrexex2  5670  dfoprab4f  5738  cbvrald  7226  bj-bdfindes  7367  bj-findes  7395