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

Theorem sban 2075
Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1865. (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 2069 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜑)
3 simpr 484 . . . 4 ((𝜑𝜓) → 𝜓)
43sbimi 2069 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜓)
52, 4jca 511 . 2 ([𝑦 / 𝑥](𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6 pm3.2 469 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76sb2imi 2070 . . 3 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑𝜓)))
87imp 406 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑𝜓))
95, 8impbii 208 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395  [wsb 2059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-an 396  df-sb 2060
This theorem is referenced by:  sb3an  2076  sbbi  2296  sbabel  2932  sbabelOLD  2933  cbvreuwOLD  3406  cbvreu  3418  rmo3f  3725  sbcan  3824  rmo3  3878  inab  4294  difab  4295  exss  5456  inopab  5822  difopab  5823  mo5f  32238  iuninc  32301  suppss2f  32372  fmptdF  32390  disjdsct  32431  esumpfinvalf  33604  measiuns  33745  ballotlemodife  34026  xpab  35229  sbn1ALT  36244  sb5ALT  43867  2uasbanh  43903  2uasbanhVD  44253  sb5ALTVD  44255  ellimcabssub0  44910  ichan  46700
  Copyright terms: Public domain W3C validator