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

Theorem sban 2077
Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1867. (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 2071 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜑)
3 simpr 484 . . . 4 ((𝜑𝜓) → 𝜓)
43sbimi 2071 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜓)
52, 4jca 511 . 2 ([𝑦 / 𝑥](𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6 pm3.2 469 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76sb2imi 2072 . . 3 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑𝜓)))
87imp 406 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑𝜓))
95, 8impbii 209 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  [wsb 2061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805
This theorem depends on definitions:  df-bi 207  df-an 396  df-sb 2062
This theorem is referenced by:  sb3an  2078  sbbi  2306  sbabel  2935  sbabelOLD  2936  cbvreuwOLD  3412  cbvreu  3424  rmo3f  3742  sbcan  3843  rmo3  3897  inab  4314  difab  4315  exss  5473  inopab  5841  difopab  5842  mo5f  32516  iuninc  32580  suppss2f  32654  fmptdF  32672  disjdsct  32717  esumpfinvalf  34056  measiuns  34197  ballotlemodife  34478  xpab  35705  sbn1ALT  36840  sb5ALT  44522  2uasbanh  44558  2uasbanhVD  44908  sb5ALTVD  44910  ellimcabssub0  45572  ichan  47379
  Copyright terms: Public domain W3C validator