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

Theorem sbequ 1813
 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 1812 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 1812 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 1685 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 128 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  [wsb 1736 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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737 This theorem is referenced by:  drsb2  1814  sbco2vlem  1918  sbco2v  1922  sbco2yz  1937  sbcocom  1944  sb10f  1971  hbsb4  1988  nfsb4or  1999  sb8eu  2013  sb8euh  2023  cbvab  2264  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvralsv  2671  cbvrexsv  2672  cbvrab  2687  cbvreucsf  3068  cbvrabcsf  3069  sbss  3475  disjiun  3931  cbvopab1  4008  cbvmpt  4030  tfis  4504  findes  4524  cbviota  5100  sb8iota  5102  cbvriota  5747  uzind4s  9411  bezoutlemmain  11720  cbvrald  13164  setindft  13332
 Copyright terms: Public domain W3C validator