Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sban Structured version   Visualization version   GIF version

Theorem sban 2475
 Description: Conjunction inside and outside of a substitution are equivalent. For a version requiring disjoint variables, but fewer axioms, see sbanv 2281. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sban ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Proof of Theorem sban
StepHypRef Expression
1 sbn 2467 . . 3 ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ [𝑦 / 𝑥](𝜑 → ¬ 𝜓))
2 sbim 2471 . . . 4 ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓))
3 sbn 2467 . . . . 5 ([𝑦 / 𝑥] ¬ 𝜓 ↔ ¬ [𝑦 / 𝑥]𝜓)
43imbi2i 328 . . . 4 (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
52, 4bitri 267 . . 3 ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
61, 5xchbinx 326 . 2 ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
7 df-an 387 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
87sbbii 2019 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓))
9 df-an 387 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
106, 8, 93bitr4i 295 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386  [wsb 2011 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-12 2163  ax-13 2334 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-sb 2012 This theorem is referenced by:  sb3an  2476  sbbi  2477  sbabel  2968  cbvreu  3365  rmo3f  3615  sbcan  3696  rmo3OLD  3746  inab  4121  difab  4122  exss  5165  inopab  5500  mo5f  29900  iuninc  29945  suppss2f  30008  fmptdF  30025  disjdsct  30050  esumpfinvalf  30740  measiuns  30882  ballotlemodife  31162  wl-dfrabf  34002  sb5ALT  39695  2uasbanh  39731  2uasbanhVD  40090  sb5ALTVD  40092  ellimcabssub0  40767
 Copyright terms: Public domain W3C validator