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

Theorem sban 2087
 Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1872. (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 486 . . . 4 ((𝜑𝜓) → 𝜑)
21sbimi 2080 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜑)
3 simpr 488 . . . 4 ((𝜑𝜓) → 𝜓)
43sbimi 2080 . . 3 ([𝑦 / 𝑥](𝜑𝜓) → [𝑦 / 𝑥]𝜓)
52, 4jca 515 . 2 ([𝑦 / 𝑥](𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6 pm3.2 473 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76sb2imi 2081 . . 3 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑𝜓)))
87imp 410 . 2 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑𝜓))
95, 8impbii 212 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  [wsb 2070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-an 400  df-sb 2071 This theorem is referenced by:  sb3an  2088  sbbi  2319  sbabel  3013  cbvreuw  3427  cbvreu  3432  rmo3f  3711  sbcan  3806  rmo3  3856  inab  4256  difab  4257  exss  5342  inopab  5688  mo5f  30266  iuninc  30327  suppss2f  30399  fmptdF  30416  disjdsct  30453  esumpfinvalf  31396  measiuns  31537  ballotlemodife  31816  wl-dfrabv  34976  wl-dfrabf  34978  sb5ALT  41156  2uasbanh  41192  2uasbanhVD  41542  sb5ALTVD  41544  ellimcabssub0  42190  ichan  43903
 Copyright terms: Public domain W3C validator