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

Theorem sban 2083
Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1873. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.)
Assertion
Ref Expression
sban ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Proof of Theorem sban
StepHypRef Expression
1 simpl 483 . . . 4 ((𝜑𝜓) → 𝜑)
21sbimi 2077 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜑)
3 simpr 485 . . . 4 ((𝜑𝜓) → 𝜓)
43sbimi 2077 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜓)
52, 4jca 512 . 2 ([𝑦 / 𝑥](𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6 pm3.2 470 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76sb2imi 2078 . . 3 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑𝜓)))
87imp 407 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑𝜓))
95, 8impbii 208 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  [wsb 2067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 397  df-sb 2068
This theorem is referenced by:  sb3an  2084  sbbi  2305  sbabel  2941  sbabelOLD  2942  cbvreuwOLD  3377  cbvreu  3381  rmo3f  3669  sbcan  3768  rmo3  3822  inab  4233  difab  4234  exss  5378  inopab  5739  mo5f  30837  iuninc  30900  suppss2f  30974  fmptdF  30993  disjdsct  31035  esumpfinvalf  32044  measiuns  32185  ballotlemodife  32464  xpab  33677  sbn1ALT  35042  sb5ALT  42145  2uasbanh  42181  2uasbanhVD  42531  sb5ALTVD  42533  ellimcabssub0  43158  ichan  44907
  Copyright terms: Public domain W3C validator