ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbequ GIF version

Theorem sbequ 1833
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 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 1832 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 1832 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 1701 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 128 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  [wsb 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756
This theorem is referenced by:  drsb2  1834  sbco2vlem  1937  sbco2v  1941  sbco2yz  1956  sbcocom  1963  sb10f  1988  hbsb4  2005  nfsb4or  2014  sb8eu  2032  sb8euh  2042  cbvab  2294  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvralsv  2712  cbvrexsv  2713  cbvrab  2728  cbvreucsf  3113  cbvrabcsf  3114  sbss  3523  disjiun  3984  cbvopab1  4062  cbvmpt  4084  tfis  4567  findes  4587  cbviota  5165  sb8iota  5167  cbvriota  5819  uzind4s  9549  bezoutlemmain  11953  cbvrald  13823  setindft  14000
  Copyright terms: Public domain W3C validator