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

Theorem sban 2387
Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sban ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Proof of Theorem sban
StepHypRef Expression
1 sbn 2379 . . 3 ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ [𝑦 / 𝑥](𝜑 → ¬ 𝜓))
2 sbim 2383 . . . 4 ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓))
3 sbn 2379 . . . . 5 ([𝑦 / 𝑥] ¬ 𝜓 ↔ ¬ [𝑦 / 𝑥]𝜓)
43imbi2i 325 . . . 4 (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
52, 4bitri 263 . . 3 ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
61, 5xchbinx 323 . 2 ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
7 df-an 385 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
87sbbii 1874 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓))
9 df-an 385 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
106, 8, 93bitr4i 291 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  [wsb 1867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868
This theorem is referenced by:  sb3an  2388  sbbi  2389  sbabel  2779  cbvreu  3145  sbcan  3445  rmo3  3494  inab  3854  difab  3855  exss  4858  inopab  5174  mo5f  28708  rmo3f  28719  iuninc  28761  suppss2f  28819  fmptdF  28836  disjdsct  28863  esumpfinvalf  29465  measiuns  29607  ballotlemodife  29886  sb5ALT  37752  sbcangOLD  37760  2uasbanh  37798  2uasbanhVD  38169  sb5ALTVD  38171  ellimcabssub0  38684
  Copyright terms: Public domain W3C validator