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

Theorem sban 2403
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 2395 . . 3 ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ [𝑦 / 𝑥](𝜑 → ¬ 𝜓))
2 sbim 2399 . . . 4 ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓))
3 sbn 2395 . . . . 5 ([𝑦 / 𝑥] ¬ 𝜓 ↔ ¬ [𝑦 / 𝑥]𝜓)
43imbi2i 326 . . . 4 (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
52, 4bitri 264 . . 3 ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
61, 5xchbinx 324 . 2 ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
7 df-an 386 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
87sbbii 1889 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓))
9 df-an 386 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
106, 8, 93bitr4i 292 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  [wsb 1882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-10 2021  ax-12 2049  ax-13 2250
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-sb 1883
This theorem is referenced by:  sb3an  2404  sbbi  2405  sbabel  2795  cbvreu  3162  sbcan  3465  rmo3  3514  inab  3876  difab  3877  exss  4897  inopab  5217  mo5f  29164  rmo3f  29175  iuninc  29215  suppss2f  29272  fmptdF  29289  disjdsct  29314  esumpfinvalf  29911  measiuns  30053  ballotlemodife  30332  sb5ALT  38180  sbcangOLD  38188  2uasbanh  38226  2uasbanhVD  38597  sb5ALTVD  38599  ellimcabssub0  39221
  Copyright terms: Public domain W3C validator