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

Theorem sban 1878
Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
Assertion
Ref Expression
sban ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Proof of Theorem sban
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 sbanv 1818 . . . 4 ([𝑧 / 𝑥](𝜑𝜓) ↔ ([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓))
21sbbii 1696 . . 3 ([𝑦 / 𝑧][𝑧 / 𝑥](𝜑𝜓) ↔ [𝑦 / 𝑧]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓))
3 sbanv 1818 . . 3 ([𝑦 / 𝑧]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓) ↔ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ∧ [𝑦 / 𝑧][𝑧 / 𝑥]𝜓))
42, 3bitri 183 . 2 ([𝑦 / 𝑧][𝑧 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ∧ [𝑦 / 𝑧][𝑧 / 𝑥]𝜓))
5 ax-17 1465 . . 3 ((𝜑𝜓) → ∀𝑧(𝜑𝜓))
65sbco2v 1870 . 2 ([𝑦 / 𝑧][𝑧 / 𝑥](𝜑𝜓) ↔ [𝑦 / 𝑥](𝜑𝜓))
7 ax-17 1465 . . . 4 (𝜑 → ∀𝑧𝜑)
87sbco2v 1870 . . 3 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
9 ax-17 1465 . . . 4 (𝜓 → ∀𝑧𝜓)
109sbco2v 1870 . . 3 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓)
118, 10anbi12i 449 . 2 (([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ∧ [𝑦 / 𝑧][𝑧 / 𝑥]𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
124, 6, 113bitr3i 209 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  [wsb 1693
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474
This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694
This theorem is referenced by:  sb3an  1881  sbbi  1882  sbmo  2008  moanim  2023  sbabel  2255  nfrexdya  2414  cbvreu  2589  rmo3f  2813  sbcan  2882  sbcang  2883  rmo3  2931  inab  3268  difab  3269  exss  4063  inopab  4581  bdcriota  12040
  Copyright terms: Public domain W3C validator