MPE Home 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