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

Theorem sban 2080
Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1870. (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 482 . . . 4 ((𝜑𝜓) → 𝜑)
21sbimi 2074 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜑)
3 simpr 484 . . . 4 ((𝜑𝜓) → 𝜓)
43sbimi 2074 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜓)
52, 4jca 511 . 2 ([𝑦 / 𝑥](𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6 pm3.2 469 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76sb2imi 2075 . . 3 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑𝜓)))
87imp 406 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑𝜓))
95, 8impbii 209 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  [wsb 2064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-sb 2065
This theorem is referenced by:  sb3an  2081  sbbi  2308  sbabel  2938  sbabelOLD  2939  cbvreuwOLD  3415  cbvreu  3428  rmo3f  3740  sbcan  3838  rmo3  3889  inab  4309  difab  4310  exss  5468  inopab  5839  difopab  5840  mo5f  32508  iuninc  32573  suppss2f  32648  fmptdF  32666  disjdsct  32712  esumpfinvalf  34077  measiuns  34218  ballotlemodife  34500  xpab  35726  sbn1ALT  36859  sb5ALT  44545  2uasbanh  44581  2uasbanhVD  44931  sb5ALTVD  44933  ellimcabssub0  45632  ichan  47442
  Copyright terms: Public domain W3C validator