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

Theorem sbequ 1851
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 1850 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 1850 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 1719 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 129 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  [wsb 1773
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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774
This theorem is referenced by:  drsb2  1852  sbco2vlem  1956  sbco2v  1960  sbco2yz  1975  sbcocom  1982  sb10f  2007  hbsb4  2024  nfsb4or  2033  sb8eu  2051  sb8euh  2061  cbvab  2313  cbvralf  2710  cbvrexf  2711  cbvreu  2716  cbvralsv  2734  cbvrexsv  2735  cbvrab  2750  cbvreucsf  3136  cbvrabcsf  3137  sbss  3546  disjiun  4013  cbvopab1  4091  cbvmpt  4113  tfis  4600  findes  4620  cbviota  5201  sb8iota  5203  cbvriota  5863  uzind4s  9622  bezoutlemmain  12034  cbvrald  15018  setindft  15195
  Copyright terms: Public domain W3C validator